Metamath Proof Explorer

Theorem an82ds

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

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

Proof

Step Hyp Ref Expression
1 an82ds.1 
 |-  ( ( ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) /\ si ) -> rh )
2 an32 
 |-  ( ( ( ph /\ ps ) /\ si ) <-> ( ( ph /\ si ) /\ ps ) )
3 2 anbi1i 
 |-  ( ( ( ( ph /\ ps ) /\ si ) /\ th ) <-> ( ( ( ph /\ si ) /\ ps ) /\ th ) )
4 3 anbi1i 
 |-  ( ( ( ( ( ph /\ ps ) /\ si ) /\ th ) /\ ta ) <-> ( ( ( ( ph /\ si ) /\ ps ) /\ th ) /\ ta ) )
5 4 anbi1i 
 |-  ( ( ( ( ( ( ph /\ ps ) /\ si ) /\ th ) /\ ta ) /\ et ) <-> ( ( ( ( ( ph /\ si ) /\ ps ) /\ th ) /\ ta ) /\ et ) )
6 5 anbi1i 
 |-  ( ( ( ( ( ( ( ph /\ ps ) /\ si ) /\ th ) /\ ta ) /\ et ) /\ ze ) <-> ( ( ( ( ( ( ph /\ si ) /\ ps ) /\ th ) /\ ta ) /\ et ) /\ ze ) )
7 1 an72ds 
 |-  ( ( ( ( ( ( ( ( ph /\ ps ) /\ si ) /\ th ) /\ ta ) /\ et ) /\ ze ) /\ ch ) -> rh )
8 6 7 sylanbr 
 |-  ( ( ( ( ( ( ( ( ph /\ si ) /\ ps ) /\ th ) /\ ta ) /\ et ) /\ ze ) /\ ch ) -> rh )
9 8 an72ds 
 |-  ( ( ( ( ( ( ( ( ph /\ si ) /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) /\ ps ) -> rh )