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  4237  unrab  4268  uniun  4884  unopab  5175  xpundi  5692  difxp  6117  coundir  6201  imadif  6570  unpreima  7001  soseq  8099  tpostpos  8186  elznn0nn  12503  faclbnd4lem4  14221  opsrtoslem1  21978  mbfmax  25566  fta1glem2  26090  ofmulrt  26205  lgsquadlem3  27309  nogesgn1o  27601  nosep1o  27609  noinfbnd2lem1  27658  difrab2  32460  ordtconnlem1  33890  ballotlemodife  34465  subfacp1lem6  35157  satf0op  35349  lineunray  36120  wl-ifpimpr  37439  wl-df2-3mintru2  37458  poimirlem30  37629  itg2addnclem2  37651  sticksstones22  42141  lzunuz  42741  diophun  42746  rmydioph  42987  fzunt  43428  fzuntd  43429  fzunt1d  43430  fzuntgd  43431  rp-isfinite6  43491  relexpxpmin  43690  andi3or  43997  clsk1indlem3  44016  simpcntrab  46852  zeoALTV  47655