This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem an62ds

Description: Inference exchanging the last antecedent with the second one. (Contributed by Thierry Arnoux, 3-Jun-2025)

Ref Expression
Hypothesis an62ds.1 
|- ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) -> ze )
Assertion an62ds 
|- ( ( ( ( ( ( ph /\ et ) /\ ch ) /\ th ) /\ ta ) /\ ps ) -> ze )

Proof

Step Hyp Ref Expression
1 an62ds.1 
 |-  ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) -> ze )
2 an32 
 |-  ( ( ( ph /\ ps ) /\ et ) <-> ( ( ph /\ et ) /\ ps ) )
3 2 anbi1i 
 |-  ( ( ( ( ph /\ ps ) /\ et ) /\ th ) <-> ( ( ( ph /\ et ) /\ ps ) /\ th ) )
4 3 anbi1i 
 |-  ( ( ( ( ( ph /\ ps ) /\ et ) /\ th ) /\ ta ) <-> ( ( ( ( ph /\ et ) /\ ps ) /\ th ) /\ ta ) )
5 1 an52ds 
 |-  ( ( ( ( ( ( ph /\ ps ) /\ et ) /\ th ) /\ ta ) /\ ch ) -> ze )
6 4 5 sylanbr 
 |-  ( ( ( ( ( ( ph /\ et ) /\ ps ) /\ th ) /\ ta ) /\ ch ) -> ze )
7 6 an52ds 
 |-  ( ( ( ( ( ( ph /\ et ) /\ ch ) /\ th ) /\ ta ) /\ ps ) -> ze )