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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862

This theorem is used by:  andir  1026  anddi  1028  cadan  1642  indi  4240  unrab  4271  uniun  4900  unopab  5196  xpundi  5735  difxp  6166  coundir  6254  imadif  6627  unpreima  7065  soseq  8164  tpostpos  8251  elznn0nn  12623  faclbnd4lem4  14352  opsrtoslem1  22243  mbfmax  25845  fta1glem2  26363  ofmulrt  26477  lgsquadlem3  27583  nogesgn1o  27874  nosep1o  27882  noinfbnd2lem1  27931  difrab2  32881  ordtconnlem1  34345  ballotlemodife  34919  subfacp1lem6  35697  satf0op  35889  lineunray  36659  bj-axseprep  37751  wl-ifpimpr  38152  wl-df2-3mintru2  38171  poimirlem30  38341  itg2addnclem2  38363  sticksstones22  42975  lzunuz  43539  diophun  43544  rmydioph  43781  fzunt  44221  fzuntd  44222  fzunt1d  44223  fzuntgd  44224  rp-isfinite6  44284  relexpxpmin  44483  andi3or  44790  clsk1indlem3  44809  simpcntrab  47624  zeoALTV  48475