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  4233  unrab  4264  uniun  4881  unopab  5173  xpundi  5688  difxp  6116  coundir  6200  imadif  6570  unpreima  7002  soseq  8095  tpostpos  8182  elznn0nn  12489  faclbnd4lem4  14205  opsrtoslem1  21991  mbfmax  25578  fta1glem2  26102  ofmulrt  26217  lgsquadlem3  27321  nogesgn1o  27613  nosep1o  27621  noinfbnd2lem1  27670  difrab2  32479  ordtconnlem1  33958  ballotlemodife  34532  subfacp1lem6  35250  satf0op  35442  lineunray  36212  wl-ifpimpr  37531  wl-df2-3mintru2  37550  poimirlem30  37710  itg2addnclem2  37732  sticksstones22  42281  lzunuz  42885  diophun  42890  rmydioph  43131  fzunt  43572  fzuntd  43573  fzunt1d  43574  fzuntgd  43575  rp-isfinite6  43635  relexpxpmin  43834  andi3or  44141  clsk1indlem3  44160  simpcntrab  46992  zeoALTV  47794