an52ds

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

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

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

Metamath Proof Explorer