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 618	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
6		olc 869	. . . 4 ⊢ (𝜒 → (𝜓 ∨ 𝜒))
7	6	anim2i 618	. . 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  1611  indi  4224  unrab  4255  uniun  4873  unopab  5165  xpundi  5700  difxp  6128  coundir  6212  imadif  6582  unpreima  7015  soseq  8109  tpostpos  8196  elznn0nn  12538  faclbnd4lem4  14258  opsrtoslem1  22033  mbfmax  25616  fta1glem2  26134  ofmulrt  26248  lgsquadlem3  27345  nogesgn1o  27637  nosep1o  27645  noinfbnd2lem1  27694  difrab2  32567  ordtconnlem1  34068  ballotlemodife  34642  subfacp1lem6  35367  satf0op  35559  lineunray  36329  bj-axseprep  37381  wl-ifpimpr  37782  wl-df2-3mintru2  37801  poimirlem30  37971  itg2addnclem2  37993  sticksstones22  42607  lzunuz  43200  diophun  43205  rmydioph  43442  fzunt  43882  fzuntd  43883  fzunt1d  43884  fzuntgd  43885  rp-isfinite6  43945  relexpxpmin  44144  andi3or  44451  clsk1indlem3  44470  simpcntrab  47298  zeoALTV  48146