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  4247  unrab  4278  uniun  4894  unopab  5187  xpundi  5707  difxp  6137  coundir  6221  imadif  6600  unpreima  7035  soseq  8138  tpostpos  8225  elznn0nn  12543  faclbnd4lem4  14261  opsrtoslem1  21962  mbfmax  25550  fta1glem2  26074  ofmulrt  26189  lgsquadlem3  27293  nogesgn1o  27585  nosep1o  27593  noinfbnd2lem1  27642  difrab2  32427  ordtconnlem1  33914  ballotlemodife  34489  subfacp1lem6  35172  satf0op  35364  lineunray  36135  wl-ifpimpr  37454  wl-df2-3mintru2  37473  poimirlem30  37644  itg2addnclem2  37666  sticksstones22  42156  lzunuz  42756  diophun  42761  rmydioph  43003  fzunt  43444  fzuntd  43445  fzunt1d  43446  fzuntgd  43447  rp-isfinite6  43507  relexpxpmin  43706  andi3or  44013  clsk1indlem3  44032  simpcntrab  46868  zeoALTV  47671