Theorem andi 1009

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 867	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
2		olc 868	. . 3 ⊢ ((𝜑 ∧ 𝜒) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
3	1, 2	jaodan 959	. 2 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
4		orc 867	. . . 4 ⊢ (𝜓 → (𝜓 ∨ 𝜒))
5	4	anim2i 617	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
6		olc 868	. . . 4 ⊢ (𝜒 → (𝜓 ∨ 𝜒))
7	6	anim2i 617	. . 3 ⊢ ((𝜑 ∧ 𝜒) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
8	5, 7	jaoi 857	. 2 ⊢ (((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
9	3, 8	impbii 209	1 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∨ wo 847

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 207  df-an 396  df-or 848

This theorem is referenced by:  andir  1010  anddi  1012  cadan  1609  indi  4259  unrab  4290  uniun  4906  unopab  5200  xpundi  5723  difxp  6153  coundir  6237  imadif  6620  unpreima  7053  soseq  8158  tpostpos  8245  elznn0nn  12602  faclbnd4lem4  14314  opsrtoslem1  22013  mbfmax  25602  fta1glem2  26126  ofmulrt  26241  lgsquadlem3  27345  nogesgn1o  27637  nosep1o  27645  noinfbnd2lem1  27694  difrab2  32479  ordtconnlem1  33955  ballotlemodife  34530  subfacp1lem6  35207  satf0op  35399  lineunray  36165  wl-ifpimpr  37484  wl-df2-3mintru2  37503  poimirlem30  37674  itg2addnclem2  37696  sticksstones22  42181  lzunuz  42791  diophun  42796  rmydioph  43038  fzunt  43479  fzuntd  43480  fzunt1d  43481  fzuntgd  43482  rp-isfinite6  43542  relexpxpmin  43741  andi3or  44048  clsk1indlem3  44067  simpcntrab  46899  zeoALTV  47684