Theorem andi 1010

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 868	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
2		olc 869	. . 3 ⊢ ((𝜑 ∧ 𝜒) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
3	1, 2	jaodan 960	. 2 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
4		orc 868	. . . 4 ⊢ (𝜓 → (𝜓 ∨ 𝜒))
5	4	anim2i 617	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
6		olc 869	. . . 4 ⊢ (𝜒 → (𝜓 ∨ 𝜒))
7	6	anim2i 617	. . 3 ⊢ ((𝜑 ∧ 𝜒) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
8	5, 7	jaoi 858	. 2 ⊢ (((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
9	3, 8	impbii 209	1 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))

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

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 849

This theorem is referenced by:  andir  1011  anddi  1013  cadan  1609  indi  4284  unrab  4315  uniun  4930  unopab  5224  xpundi  5754  difxp  6184  coundir  6268  imadif  6650  unpreima  7083  soseq  8184  tpostpos  8271  elznn0nn  12627  faclbnd4lem4  14335  opsrtoslem1  22079  mbfmax  25684  fta1glem2  26208  ofmulrt  26323  lgsquadlem3  27426  nogesgn1o  27718  nosep1o  27726  noinfbnd2lem1  27775  difrab2  32517  ordtconnlem1  33923  ballotlemodife  34500  subfacp1lem6  35190  satf0op  35382  lineunray  36148  wl-ifpimpr  37467  wl-df2-3mintru2  37486  poimirlem30  37657  itg2addnclem2  37679  sticksstones22  42169  lzunuz  42779  diophun  42784  rmydioph  43026  fzunt  43468  fzuntd  43469  fzunt1d  43470  fzuntgd  43471  rp-isfinite6  43531  relexpxpmin  43730  andi3or  44037  clsk1indlem3  44056  simpcntrab  46885  zeoALTV  47657