dfbi3

Description: An alternate definition of the biconditional. Theorem *5.23 of WhiteheadRussell p. 124. (Contributed by NM, 27-Jun-2002) (Proof shortened by Wolf Lammen, 3-Nov-2013) (Proof shortened by NM, 29-Oct-2021)

		Ref	Expression
	Assertion	dfbi3	$⊢ (φ \leftrightarrow ψ) \leftrightarrow ((φ \land ψ) \lor (\neg φ \land \neg ψ))$

Proof

Step	Hyp	Ref	Expression
1		con34b	$⊢ (ψ \to φ) \leftrightarrow (\neg φ \to \neg ψ)$
2	1	anbi2i	$⊢ ((φ \to ψ) \land (ψ \to φ)) \leftrightarrow ((φ \to ψ) \land (\neg φ \to \neg ψ))$
3		dfbi2	$⊢ (φ \leftrightarrow ψ) \leftrightarrow ((φ \to ψ) \land (ψ \to φ))$
4		cases2	$⊢ ((φ \land ψ) \lor (\neg φ \land \neg ψ)) \leftrightarrow ((φ \to ψ) \land (\neg φ \to \neg ψ))$
5	2 3 4	3bitr4i	$⊢ (φ \leftrightarrow ψ) \leftrightarrow ((φ \land ψ) \lor (\neg φ \land \neg ψ))$

Metamath Proof Explorer

Theorem dfbi3

Proof