Theorem dfbi 499

Description: An alternate definition of the biconditional. Theorem *5.23 of [WhiteheadRussell] p. 124.

Assertion

Ref	Expression
dfbi	⊢ ((φ ↔ ψ) ↔ ((φ ∧ ψ) ∨ (¬ φ ∧ ¬ ψ)))

Proof of Theorem dfbi

Step	Hyp	Ref	Expression
1		pm5.18 497	. 2 ⊢ ((φ ↔ ψ) ↔ ¬ (φ ↔ ¬ ψ))
2		imnan 207	. . . . 5 ⊢ ((φ → ¬ ψ) ↔ ¬ (φ ∧ ψ))
3		bi2.15 145	. . . . . 6 ⊢ ((¬ ψ → φ) ↔ (¬ φ → ψ))
4		iman 205	. . . . . 6 ⊢ ((¬ φ → ψ) ↔ ¬ (¬ φ ∧ ¬ ψ))
5	3, 4	bitr 151	. . . . 5 ⊢ ((¬ ψ → φ) ↔ ¬ (¬ φ ∧ ¬ ψ))
6	2, 5	anbi12i 369	. . . 4 ⊢ (((φ → ¬ ψ) ∧ (¬ ψ → φ)) ↔ (¬ (φ ∧ ψ) ∧ ¬ (¬ φ ∧ ¬ ψ)))
7		bi 396	. . . 4 ⊢ ((φ ↔ ¬ ψ) ↔ ((φ → ¬ ψ) ∧ (¬ ψ → φ)))
8		ioran 254	. . . 4 ⊢ (¬ ((φ ∧ ψ) ∨ (¬ φ ∧ ¬ ψ)) ↔ (¬ (φ ∧ ψ) ∧ ¬ (¬ φ ∧ ¬ ψ)))
9	6, 7, 8	3bitr4r 159	. . 3 ⊢ (¬ ((φ ∧ ψ) ∨ (¬ φ ∧ ¬ ψ)) ↔ (φ ↔ ¬ ψ))
10	9	bicon1i 193	. 2 ⊢ (¬ (φ ↔ ¬ ψ) ↔ ((φ ∧ ψ) ∨ (¬ φ ∧ ¬ ψ)))
11	1, 10	bitr 151	1 ⊢ ((φ ↔ ψ) ↔ ((φ ∧ ψ) ∨ (¬ φ ∧ ¬ ψ)))

Syntax hints:  ¬ wn 1   → wi 2   ↔ wb 127   ∨ wo 195   ∧ wa 196

This theorem is referenced by:  xor 500  biass 511  symdif2 1690  ifbi 1783

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198

metamath.org