Theorem andi 1008

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

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

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 847

This theorem is referenced by:  andir  1009  anddi  1011  cadan  1606  indi  4303  unrab  4334  uniun  4954  unopab  5248  xpundi  5768  difxp  6195  coundir  6279  imadif  6662  unpreima  7096  soseq  8200  tpostpos  8287  elznn0nn  12653  faclbnd4lem4  14345  opsrtoslem1  22102  mbfmax  25703  fta1glem2  26228  ofmulrt  26341  lgsquadlem3  27444  nogesgn1o  27736  nosep1o  27744  noinfbnd2lem1  27793  difrab2  32526  ordtconnlem1  33870  ballotlemodife  34462  subfacp1lem6  35153  satf0op  35345  lineunray  36111  wl-ifpimpr  37432  wl-df2-3mintru2  37451  poimirlem30  37610  itg2addnclem2  37632  sticksstones22  42125  lzunuz  42724  diophun  42729  rmydioph  42971  fzunt  43417  fzuntd  43418  fzunt1d  43419  fzuntgd  43420  rp-isfinite6  43480  relexpxpmin  43679  andi3or  43986  clsk1indlem3  44005  simpcntrab  46791  zeoALTV  47544