Theorem an72ds

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

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

Proof

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