pm5.71

		Ref	Expression
	Assertion	pm5.71	$⊢ (ψ \to \neg χ) \to (((φ \lor ψ) \land χ) \leftrightarrow (φ \land χ))$

Step	Hyp	Ref	Expression
1		orel2	$⊢ \neg ψ \to ((φ \lor ψ) \to φ)$
2		orc	$⊢ φ \to (φ \lor ψ)$
3	1 2	impbid1	$⊢ \neg ψ \to ((φ \lor ψ) \leftrightarrow φ)$
4	3	anbi1d	$⊢ \neg ψ \to (((φ \lor ψ) \land χ) \leftrightarrow (φ \land χ))$
5		pm2.21	$⊢ \neg χ \to (χ \to ((φ \lor ψ) \leftrightarrow φ))$
6	5	pm5.32rd	$⊢ \neg χ \to (((φ \lor ψ) \land χ) \leftrightarrow (φ \land χ))$
7	4 6	ja	$⊢ (ψ \to \neg χ) \to (((φ \lor ψ) \land χ) \leftrightarrow (φ \land χ))$

Metamath Proof Explorer