Metamath Proof Explorer

Theorem pm5.32rd

Description: Distribution of implication over biconditional (deduction form). (Contributed by NM, 25-Dec-2004)

		Ref	Expression
	Hypothesis	pm5.32d.1	$⊢ φ \to (ψ \to (χ \leftrightarrow θ))$
	Assertion	pm5.32rd	$⊢ φ \to ((χ \land ψ) \leftrightarrow (θ \land ψ))$

Step	Hyp	Ref	Expression
1		pm5.32d.1	$⊢ φ \to (ψ \to (χ \leftrightarrow θ))$
2	1	pm5.32d	$⊢ φ \to ((ψ \land χ) \leftrightarrow (ψ \land θ))$
3		ancom	$⊢ (χ \land ψ) \leftrightarrow (ψ \land χ)$
4		ancom	$⊢ (θ \land ψ) \leftrightarrow (ψ \land θ)$
5	2 3 4	3bitr4g	$⊢ φ \to ((χ \land ψ) \leftrightarrow (θ \land ψ))$