an72ds

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

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

Step	Hyp	Ref	Expression
1		an72ds.1	$⊢ ((((((φ \land ψ) \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	4	anbi1i	$⊢ (((((φ \land ψ) \land ζ) \land θ) \land τ) \land η) \leftrightarrow (((((φ \land ζ) \land ψ) \land θ) \land τ) \land η)$
6	1	an62ds	$⊢ ((((((φ \land ψ) \land ζ) \land θ) \land τ) \land η) \land χ) \to σ$
7	5 6	sylanbr	$⊢ ((((((φ \land ζ) \land ψ) \land θ) \land τ) \land η) \land χ) \to σ$
8	7	an62ds	$⊢ ((((((φ \land ζ) \land χ) \land θ) \land τ) \land η) \land ψ) \to σ$

Metamath Proof Explorer