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  1610  indi  4234  unrab  4265  uniun  4882  unopab  5171  xpundi  5685  difxp  6111  coundir  6195  imadif  6565  unpreima  6996  soseq  8089  tpostpos  8176  elznn0nn  12479  faclbnd4lem4  14200  opsrtoslem1  21988  mbfmax  25575  fta1glem2  26099  ofmulrt  26214  lgsquadlem3  27318  nogesgn1o  27610  nosep1o  27618  noinfbnd2lem1  27667  difrab2  32472  ordtconnlem1  33932  ballotlemodife  34506  subfacp1lem6  35217  satf0op  35409  lineunray  36180  wl-ifpimpr  37499  wl-df2-3mintru2  37518  poimirlem30  37689  itg2addnclem2  37711  sticksstones22  42200  lzunuz  42800  diophun  42805  rmydioph  43046  fzunt  43487  fzuntd  43488  fzunt1d  43489  fzuntgd  43490  rp-isfinite6  43550  relexpxpmin  43749  andi3or  44056  clsk1indlem3  44075  simpcntrab  46907  zeoALTV  47700