Theorem andi 1004

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 863	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
2		olc 864	. . 3 ⊢ ((𝜑 ∧ 𝜒) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
3	1, 2	jaodan 954	. 2 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
4		orc 863	. . . 4 ⊢ (𝜓 → (𝜓 ∨ 𝜒))
5	4	anim2i 616	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
6		olc 864	. . . 4 ⊢ (𝜒 → (𝜓 ∨ 𝜒))
7	6	anim2i 616	. . 3 ⊢ ((𝜑 ∧ 𝜒) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
8	5, 7	jaoi 853	. 2 ⊢ (((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
9	3, 8	impbii 208	1 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))

Syntax hints:   ↔ wb 205   ∧ wa 395   ∨ wo 843

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 206  df-an 396  df-or 844

This theorem is referenced by:  andir  1005  anddi  1007  cadan  1612  indi  4204  indifdirOLD  4216  unrab  4236  uniprOLD  4855  uniun  4861  unopab  5152  xpundi  5646  difxp  6056  coundir  6141  imadif  6502  unpreima  6922  tpostpos  8033  elznn0nn  12263  faclbnd4lem4  13938  opsrtoslem1  21172  mbfmax  24718  fta1glem2  25236  ofmulrt  25347  lgsquadlem3  26435  difrab2  30746  ordtconnlem1  31776  ballotlemodife  32364  subfacp1lem6  33047  satf0op  33239  soseq  33730  nogesgn1o  33803  nosep1o  33811  noinfbnd2lem1  33860  lineunray  34376  wl-ifpimpr  35564  wl-df2-3mintru2  35583  poimirlem30  35734  itg2addnclem2  35756  sticksstones22  40052  lzunuz  40506  diophun  40511  rmydioph  40752  rp-isfinite6  41023  relexpxpmin  41214  andi3or  41521  clsk1indlem3  41542  simpcntrab  44273  zeoALTV  45010