Theorem andi 1030

Description: Distributive law for conjunction. Theorem *4.4 of [WhiteheadRussell] p. 118. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 5-Jan-2013.)

Assertion

Ref	Expression
andi	⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))

Proof of Theorem andi

Step	Hyp	Ref	Expression
1		orc 893	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
2		olc 894	. . 3 ⊢ ((𝜑 ∧ 𝜒) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
3	1, 2	jaodan 980	. 2 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
4		orc 893	. . . 4 ⊢ (𝜓 → (𝜓 ∨ 𝜒))
5	4	anim2i 610	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
6		olc 894	. . . 4 ⊢ (𝜒 → (𝜓 ∨ 𝜒))
7	6	anim2i 610	. . 3 ⊢ ((𝜑 ∧ 𝜒) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
8	5, 7	jaoi 883	. 2 ⊢ (((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
9	3, 8	impbii 200	1 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))

Syntax hints:   ↔ wb 197   ∧ wa 384   ∨ wo 873

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

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874

This theorem is referenced by:  andir  1031  anddi  1033  annotanannotOLD  1034  cadan  1718  indi  4040  indifdir  4050  unrab  4064  unipr  4609  uniun  4617  unopab  4889  xpundi  5341  difxp  5743  coundir  5825  imadif  6153  unpreima  6535  tpostpos  7579  elznn0nn  11642  faclbnd4lem4  13292  opsrtoslem1  19771  mbfmax  23721  fta1glem2  24231  ofmulrt  24342  lgsquadlem3  25412  difrab2  29809  ordtconnlem1  30438  ballotlemodife  31028  subfacp1lem6  31636  soseq  32219  nosep1o  32297  lineunray  32719  bj-ismooredr2  33514  poimirlem30  33884  itg2addnclem2  33906  lzunuz  38033  diophun  38039  rmydioph  38282  rp-isfinite6  38563  relexpxpmin  38708  andi3or  39018  clsk1indlem3  39039  zeoALTV  42281