bj-dfbi6

Description: Alternate definition of the biconditional. (Contributed by BJ, 4-Oct-2019)

		Ref	Expression
	Assertion	bj-dfbi6	$⊢ (φ \leftrightarrow ψ) \leftrightarrow ((φ \lor ψ) \leftrightarrow (φ \land ψ))$

Step	Hyp	Ref	Expression
1		bj-dfbi5	$⊢ (φ \leftrightarrow ψ) \leftrightarrow ((φ \lor ψ) \to (φ \land ψ))$
2		id	$⊢ ((φ \lor ψ) \to (φ \land ψ)) \to ((φ \lor ψ) \to (φ \land ψ))$
3		animorr	$⊢ (φ \land ψ) \to (φ \lor ψ)$
4	2 3	impbid1	$⊢ ((φ \lor ψ) \to (φ \land ψ)) \to ((φ \lor ψ) \leftrightarrow (φ \land ψ))$
5		biimp	$⊢ ((φ \lor ψ) \leftrightarrow (φ \land ψ)) \to ((φ \lor ψ) \to (φ \land ψ))$
6	4 5	impbii	$⊢ ((φ \lor ψ) \to (φ \land ψ)) \leftrightarrow ((φ \lor ψ) \leftrightarrow (φ \land ψ))$
7	1 6	bitri	$⊢ (φ \leftrightarrow ψ) \leftrightarrow ((φ \lor ψ) \leftrightarrow (φ \land ψ))$

Metamath Proof Explorer