an62ds

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

		Ref	Expression
	Hypothesis	an62ds.1	$⊢ (((((φ \land ψ) \land χ) \land θ) \land τ) \land η) \to ζ$
	Assertion	an62ds	$⊢ (((((φ \land η) \land χ) \land θ) \land τ) \land ψ) \to ζ$

Step	Hyp	Ref	Expression
1		an62ds.1	$⊢ (((((φ \land ψ) \land χ) \land θ) \land τ) \land η) \to ζ$
2		an32	$⊢ ((φ \land ψ) \land η) \leftrightarrow ((φ \land η) \land ψ)$
3	2	anbi1i	$⊢ (((φ \land ψ) \land η) \land θ) \leftrightarrow (((φ \land η) \land ψ) \land θ)$
4	3	anbi1i	$⊢ ((((φ \land ψ) \land η) \land θ) \land τ) \leftrightarrow ((((φ \land η) \land ψ) \land θ) \land τ)$
5	1	an52ds	$⊢ (((((φ \land ψ) \land η) \land θ) \land τ) \land χ) \to ζ$
6	4 5	sylanbr	$⊢ (((((φ \land η) \land ψ) \land θ) \land τ) \land χ) \to ζ$
7	6	an52ds	$⊢ (((((φ \land η) \land χ) \land θ) \land τ) \land ψ) \to ζ$

Metamath Proof Explorer