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  1641  indi  4229  unrab  4260  uniun  4889  unopab  5184  xpundi  5719  difxp  6154  coundir  6249  imadif  6624  unpreima  7062  soseq  8178  tpostpos  8266  elznn0nn  12710  faclbnd4lem4  14443  opsrtoslem1  22369  mbfmax  25975  fta1glem2  26492  ofmulrt  26605  lgsquadlem3  27714  nogesgn1o  28035  nosep1o  28043  noinfbnd2lem1  28092  difrab2  33141  ordtconnlem1  34602  ballotlemodife  35176  subfacp1lem6  36036  satf0op  36228  lineunray  37004  bj-axseprep  38082  wl-ifpimpr  38482  wl-df2-3mintru2  38501  poimirlem30  38661  itg2addnclem2  38683  sticksstones22  43311  lzunuz  43872  diophun  43877  rmydioph  44114  fzunt  44549  fzuntd  44550  fzunt1d  44551  fzuntgd  44552  rp-isfinite6  44612  relexpxpmin  44810  andi3or  45117  clsk1indlem3  45136  simpcntrab  47973  zeoALTV  48861  prelrrx2b  49920