Theorem andi 1020

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 878	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
2		olc 879	. . 3 ⊢ ((𝜑 ∧ 𝜒) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
3	1, 2	jaodan 970	. 2 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
4		orc 878	. . . 4 ⊢ (𝜓 → (𝜓 ∨ 𝜒))
5	4	anim2i 626	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
6		olc 879	. . . 4 ⊢ (𝜒 → (𝜓 ∨ 𝜒))
7	6	anim2i 626	. . 3 ⊢ ((𝜑 ∧ 𝜒) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
8	5, 7	jaoi 868	. 2 ⊢ (((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
9	3, 8	impbii 211	1 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))

Syntax hints:   ↔ wb 208   ∧ wa 399   ∨ wo 858

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 209  df-an 400  df-or 859

This theorem is referenced by:  andir  1021  anddi  1023  cadan  1628  indi  4236  unrab  4267  uniun  4887  unopab  5179  xpundi  5714  difxp  6146  coundir  6231  imadif  6601  unpreima  7040  soseq  8134  tpostpos  8221  elznn0nn  12579  faclbnd4lem4  14306  opsrtoslem1  22088  mbfmax  25691  fta1glem2  26209  ofmulrt  26323  lgsquadlem3  27423  nogesgn1o  27714  nosep1o  27722  noinfbnd2lem1  27771  difrab2  32645  ordtconnlem1  34182  ballotlemodife  34756  subfacp1lem6  35499  satf0op  35691  lineunray  36461  bj-axseprep  37523  wl-ifpimpr  37924  wl-df2-3mintru2  37943  poimirlem30  38113  itg2addnclem2  38135  sticksstones22  42749  lzunuz  43313  diophun  43318  rmydioph  43555  fzunt  43995  fzuntd  43996  fzunt1d  43997  fzuntgd  43998  rp-isfinite6  44058  relexpxpmin  44257  andi3or  44564  clsk1indlem3  44583  simpcntrab  47408  zeoALTV  48256