Theorem andi 1025

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 880	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
2		olc 881	. . 3 ⊢ ((𝜑 ∧ 𝜒) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
3	1, 2	jaodan 972	. 2 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
4		orc 880	. . . 4 ⊢ (𝜓 → (𝜓 ∨ 𝜒))
5	4	anim2i 628	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
6		olc 881	. . . 4 ⊢ (𝜒 → (𝜓 ∨ 𝜒))
7	6	anim2i 628	. . 3 ⊢ ((𝜑 ∧ 𝜒) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
8	5, 7	jaoi 870	. 2 ⊢ (((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
9	3, 8	impbii 212	1 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))

Syntax hints:   ↔ wb 209   ∧ wa 400   ∨ wo 860

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 210  df-an 401  df-or 861

This theorem is referenced by:  andir  1026  anddi  1028  cadan  1639  indi  4238  unrab  4269  uniun  4896  unopab  5192  xpundi  5732  difxp  6163  coundir  6251  imadif  6622  unpreima  7060  soseq  8156  tpostpos  8243  elznn0nn  12606  faclbnd4lem4  14334  opsrtoslem1  22187  mbfmax  25789  fta1glem2  26307  ofmulrt  26421  lgsquadlem3  27524  nogesgn1o  27815  nosep1o  27823  noinfbnd2lem1  27872  difrab2  32822  ordtconnlem1  34292  ballotlemodife  34866  subfacp1lem6  35655  satf0op  35847  lineunray  36617  bj-axseprep  37689  wl-ifpimpr  38090  wl-df2-3mintru2  38109  poimirlem30  38279  itg2addnclem2  38301  sticksstones22  42913  lzunuz  43479  diophun  43484  rmydioph  43721  fzunt  44161  fzuntd  44162  fzunt1d  44163  fzuntgd  44164  rp-isfinite6  44224  relexpxpmin  44423  andi3or  44730  clsk1indlem3  44749  simpcntrab  47564  zeoALTV  48412