Theorem andi 1006

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

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

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 847

This theorem is referenced by:  andir  1007  anddi  1009  cadan  1603  indi  4274  indifdirOLD  4286  unrab  4306  uniprOLD  4926  uniun  4933  unopab  5230  xpundi  5746  difxp  6168  coundir  6252  imadif  6637  unpreima  7072  soseq  8164  tpostpos  8252  elznn0nn  12603  faclbnd4lem4  14288  opsrtoslem1  21999  mbfmax  25591  fta1glem2  26116  ofmulrt  26229  lgsquadlem3  27328  nogesgn1o  27619  nosep1o  27627  noinfbnd2lem1  27676  difrab2  32309  ordtconnlem1  33525  ballotlemodife  34117  subfacp1lem6  34795  satf0op  34987  lineunray  35743  wl-ifpimpr  36945  wl-df2-3mintru2  36964  poimirlem30  37123  itg2addnclem2  37145  sticksstones22  41640  lzunuz  42188  diophun  42193  rmydioph  42435  fzunt  42885  fzuntd  42886  fzunt1d  42887  fzuntgd  42888  rp-isfinite6  42948  relexpxpmin  43147  andi3or  43454  clsk1indlem3  43473  simpcntrab  46258  zeoALTV  47010

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »