Theorem andi 1007

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

Syntax hints:   ↔ wb 205   ∧ wa 397   ∨ 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 206  df-an 398  df-or 847

This theorem is referenced by:  andir  1008  anddi  1010  cadan  1611  indi  4274  indifdirOLD  4286  unrab  4306  uniprOLD  4928  uniun  4935  unopab  5231  xpundi  5745  difxp  6164  coundir  6248  imadif  6633  unpreima  7065  soseq  8145  tpostpos  8231  elznn0nn  12572  faclbnd4lem4  14256  opsrtoslem1  21616  mbfmax  25166  fta1glem2  25684  ofmulrt  25795  lgsquadlem3  26885  nogesgn1o  27176  nosep1o  27184  noinfbnd2lem1  27233  difrab2  31738  ordtconnlem1  32904  ballotlemodife  33496  subfacp1lem6  34176  satf0op  34368  lineunray  35119  wl-ifpimpr  36347  wl-df2-3mintru2  36366  poimirlem30  36518  itg2addnclem2  36540  sticksstones22  40984  lzunuz  41506  diophun  41511  rmydioph  41753  fzunt  42206  fzuntd  42207  fzunt1d  42208  fzuntgd  42209  rp-isfinite6  42269  relexpxpmin  42468  andi3or  42775  clsk1indlem3  42794  simpcntrab  45586  zeoALTV  46338