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 )