an82ds

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

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

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

Metamath Proof Explorer