Theorem andi 1005

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

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

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 845

This theorem is referenced by:  andir  1006  anddi  1008  cadan  1611  indi  4207  indifdirOLD  4219  unrab  4239  uniprOLD  4858  uniun  4864  unopab  5156  xpundi  5655  difxp  6067  coundir  6152  imadif  6518  unpreima  6940  tpostpos  8062  elznn0nn  12333  faclbnd4lem4  14010  opsrtoslem1  21262  mbfmax  24813  fta1glem2  25331  ofmulrt  25442  lgsquadlem3  26530  difrab2  30845  ordtconnlem1  31874  ballotlemodife  32464  subfacp1lem6  33147  satf0op  33339  soseq  33803  nogesgn1o  33876  nosep1o  33884  noinfbnd2lem1  33933  lineunray  34449  wl-ifpimpr  35637  wl-df2-3mintru2  35656  poimirlem30  35807  itg2addnclem2  35829  sticksstones22  40124  lzunuz  40590  diophun  40595  rmydioph  40836  fzunt  41062  fzuntd  41063  fzunt1d  41064  fzuntgd  41065  rp-isfinite6  41125  relexpxpmin  41325  andi3or  41632  clsk1indlem3  41653  simpcntrab  44386  zeoALTV  45122