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

Metamath Proof Explorer

Theorem an42ds

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

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

Proof

Step Hyp Ref Expression
1 an42ds.1 
 |-  ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ta )
2 an32 
 |-  ( ( ( ph /\ ps ) /\ th ) <-> ( ( ph /\ th ) /\ ps ) )
3 2 anbi1i 
 |-  ( ( ( ( ph /\ ps ) /\ th ) /\ ch ) <-> ( ( ( ph /\ th ) /\ ps ) /\ ch ) )
4 an32 
 |-  ( ( ( ( ph /\ ps ) /\ th ) /\ ch ) <-> ( ( ( ph /\ ps ) /\ ch ) /\ th ) )
5 an32 
 |-  ( ( ( ( ph /\ th ) /\ ps ) /\ ch ) <-> ( ( ( ph /\ th ) /\ ch ) /\ ps ) )
6 3 4 5 3bitr3i 
 |-  ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) <-> ( ( ( ph /\ th ) /\ ch ) /\ ps ) )
7 6 1 sylbir 
 |-  ( ( ( ( ph /\ th ) /\ ch ) /\ ps ) -> ta )