Metamath Proof Explorer

Theorem pm5.54

Description: Theorem *5.54 of WhiteheadRussell p. 125. (Contributed by NM, 3-Jan-2005) (Proof shortened by Wolf Lammen, 7-Nov-2013)

		Ref	Expression
	Assertion	pm5.54	$⊢ (((φ \land ψ) \leftrightarrow φ) \lor ((φ \land ψ) \leftrightarrow ψ))$

Step	Hyp	Ref	Expression
1		iba	$⊢ ψ \to (φ \leftrightarrow (φ \land ψ))$
2	1	bicomd	$⊢ ψ \to ((φ \land ψ) \leftrightarrow φ)$
3	2	adantl	$⊢ (φ \land ψ) \to ((φ \land ψ) \leftrightarrow φ)$
4	3 2	pm5.21ni	$⊢ \neg ((φ \land ψ) \leftrightarrow φ) \to ((φ \land ψ) \leftrightarrow ψ)$
5	4	orri	$⊢ (((φ \land ψ) \leftrightarrow φ) \lor ((φ \land ψ) \leftrightarrow ψ))$