MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  andi Structured version   Visualization version   GIF version

Theorem andi 1030
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
StepHypRef Expression
1 orc 893 . . 3 ((𝜑𝜓) → ((𝜑𝜓) ∨ (𝜑𝜒)))
2 olc 894 . . 3 ((𝜑𝜒) → ((𝜑𝜓) ∨ (𝜑𝜒)))
31, 2jaodan 980 . 2 ((𝜑 ∧ (𝜓𝜒)) → ((𝜑𝜓) ∨ (𝜑𝜒)))
4 orc 893 . . . 4 (𝜓 → (𝜓𝜒))
54anim2i 610 . . 3 ((𝜑𝜓) → (𝜑 ∧ (𝜓𝜒)))
6 olc 894 . . . 4 (𝜒 → (𝜓𝜒))
76anim2i 610 . . 3 ((𝜑𝜒) → (𝜑 ∧ (𝜓𝜒)))
85, 7jaoi 883 . 2 (((𝜑𝜓) ∨ (𝜑𝜒)) → (𝜑 ∧ (𝜓𝜒)))
93, 8impbii 200 1 ((𝜑 ∧ (𝜓𝜒)) ↔ ((𝜑𝜓) ∨ (𝜑𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wb 197  wa 384  wo 873
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 198  df-an 385  df-or 874
This theorem is referenced by:  andir  1031  anddi  1033  annotanannotOLD  1034  cadan  1718  indi  4040  indifdir  4050  unrab  4064  unipr  4609  uniun  4617  unopab  4889  xpundi  5341  difxp  5743  coundir  5825  imadif  6153  unpreima  6535  tpostpos  7579  elznn0nn  11642  faclbnd4lem4  13292  opsrtoslem1  19771  mbfmax  23721  fta1glem2  24231  ofmulrt  24342  lgsquadlem3  25412  difrab2  29809  ordtconnlem1  30438  ballotlemodife  31028  subfacp1lem6  31636  soseq  32219  nosep1o  32297  lineunray  32719  bj-ismooredr2  33514  poimirlem30  33884  itg2addnclem2  33906  lzunuz  38033  diophun  38039  rmydioph  38282  rp-isfinite6  38563  relexpxpmin  38708  andi3or  39018  clsk1indlem3  39039  zeoALTV  42281
  Copyright terms: Public domain W3C validator