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  4250  unrab  4281  uniun  4897  unopab  5190  xpundi  5710  difxp  6140  coundir  6224  imadif  6603  unpreima  7038  soseq  8141  tpostpos  8228  elznn0nn  12550  faclbnd4lem4  14268  opsrtoslem1  21969  mbfmax  25557  fta1glem2  26081  ofmulrt  26196  lgsquadlem3  27300  nogesgn1o  27592  nosep1o  27600  noinfbnd2lem1  27649  difrab2  32434  ordtconnlem1  33921  ballotlemodife  34496  subfacp1lem6  35179  satf0op  35371  lineunray  36142  wl-ifpimpr  37461  wl-df2-3mintru2  37480  poimirlem30  37651  itg2addnclem2  37673  sticksstones22  42163  lzunuz  42763  diophun  42768  rmydioph  43010  fzunt  43451  fzuntd  43452  fzunt1d  43453  fzuntgd  43454  rp-isfinite6  43514  relexpxpmin  43713  andi3or  44020  clsk1indlem3  44039  simpcntrab  46875  zeoALTV  47675