Theorem andi 456

Description: Distributive law for conjunction. Theorem *4.4 of [WhiteheadRussell] p. 118.

Assertion

Ref	Expression
andi	⊢ ((φ ∧ (ψ ∨ χ)) ↔ ((φ ∧ ψ) ∨ (φ ∧ χ)))

Proof of Theorem andi

Step	Hyp	Ref	Expression
1		ordi 452	. . . 4 ⊢ ((¬ φ ∨ (¬ ψ ∧ ¬ χ)) ↔ ((¬ φ ∨ ¬ ψ) ∧ (¬ φ ∨ ¬ χ)))
2		ioran 254	. . . . 5 ⊢ (¬ (ψ ∨ χ) ↔ (¬ ψ ∧ ¬ χ))
3	2	orbi2i 214	. . . 4 ⊢ ((¬ φ ∨ ¬ (ψ ∨ χ)) ↔ (¬ φ ∨ (¬ ψ ∧ ¬ χ)))
4		ianor 253	. . . . 5 ⊢ (¬ (φ ∧ ψ) ↔ (¬ φ ∨ ¬ ψ))
5		ianor 253	. . . . 5 ⊢ (¬ (φ ∧ χ) ↔ (¬ φ ∨ ¬ χ))
6	4, 5	anbi12i 369	. . . 4 ⊢ ((¬ (φ ∧ ψ) ∧ ¬ (φ ∧ χ)) ↔ ((¬ φ ∨ ¬ ψ) ∧ (¬ φ ∨ ¬ χ)))
7	1, 3, 6	3bitr4 158	. . 3 ⊢ ((¬ φ ∨ ¬ (ψ ∨ χ)) ↔ (¬ (φ ∧ ψ) ∧ ¬ (φ ∧ χ)))
8	7	negbii 162	. 2 ⊢ (¬ (¬ φ ∨ ¬ (ψ ∨ χ)) ↔ ¬ (¬ (φ ∧ ψ) ∧ ¬ (φ ∧ χ)))
9		anor 252	. 2 ⊢ ((φ ∧ (ψ ∨ χ)) ↔ ¬ (¬ φ ∨ ¬ (ψ ∨ χ)))
10		oran 255	. 2 ⊢ (((φ ∧ ψ) ∨ (φ ∧ χ)) ↔ ¬ (¬ (φ ∧ ψ) ∧ ¬ (φ ∧ χ)))
11	8, 9, 10	3bitr4 158	1 ⊢ ((φ ∧ (ψ ∨ χ)) ↔ ((φ ∧ ψ) ∨ (φ ∧ χ)))

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

This theorem is referenced by:  andir 457  anddi 459  biass 511  caselem 561  prlem2 577  r19.43 1304  indi 1676  unrab 1694  unpr 1930  uniun 1934  unopab 2121  ordnbtwn 2316  onzsl 2367  xpundi 2461  imadif 2714  phplem4 3406  ssnn 3429  elznn0nn 4575  elnn0nn 4593

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