Theorem andi 1006

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 865	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
2		olc 866	. . 3 ⊢ ((𝜑 ∧ 𝜒) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
3	1, 2	jaodan 956	. 2 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
4		orc 865	. . . 4 ⊢ (𝜓 → (𝜓 ∨ 𝜒))
5	4	anim2i 617	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
6		olc 866	. . . 4 ⊢ (𝜒 → (𝜓 ∨ 𝜒))
7	6	anim2i 617	. . 3 ⊢ ((𝜑 ∧ 𝜒) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
8	5, 7	jaoi 855	. 2 ⊢ (((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
9	3, 8	impbii 208	1 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))

Syntax hints:   ↔ wb 205   ∧ wa 396   ∨ wo 845

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 206  df-an 397  df-or 846

This theorem is referenced by:  andir  1007  anddi  1009  cadan  1610  indi  4272  indifdirOLD  4284  unrab  4304  uniprOLD  4926  uniun  4933  unopab  5229  xpundi  5742  difxp  6160  coundir  6244  imadif  6629  unpreima  7061  soseq  8141  tpostpos  8227  elznn0nn  12568  faclbnd4lem4  14252  opsrtoslem1  21607  mbfmax  25157  fta1glem2  25675  ofmulrt  25786  lgsquadlem3  26874  nogesgn1o  27165  nosep1o  27173  noinfbnd2lem1  27222  difrab2  31725  ordtconnlem1  32892  ballotlemodife  33484  subfacp1lem6  34164  satf0op  34356  lineunray  35107  wl-ifpimpr  36335  wl-df2-3mintru2  36354  poimirlem30  36506  itg2addnclem2  36528  sticksstones22  40972  lzunuz  41491  diophun  41496  rmydioph  41738  fzunt  42191  fzuntd  42192  fzunt1d  42193  fzuntgd  42194  rp-isfinite6  42254  relexpxpmin  42453  andi3or  42760  clsk1indlem3  42779  simpcntrab  45572  zeoALTV  46324