an42ds

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

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

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

Metamath Proof Explorer