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

Theorem andi 947
 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 399 . . 3 ((𝜑𝜓) → ((𝜑𝜓) ∨ (𝜑𝜒)))
2 olc 398 . . 3 ((𝜑𝜒) → ((𝜑𝜓) ∨ (𝜑𝜒)))
31, 2jaodan 861 . 2 ((𝜑 ∧ (𝜓𝜒)) → ((𝜑𝜓) ∨ (𝜑𝜒)))
4 orc 399 . . . 4 (𝜓 → (𝜓𝜒))
54anim2i 594 . . 3 ((𝜑𝜓) → (𝜑 ∧ (𝜓𝜒)))
6 olc 398 . . . 4 (𝜒 → (𝜓𝜒))
76anim2i 594 . . 3 ((𝜑𝜒) → (𝜑 ∧ (𝜓𝜒)))
85, 7jaoi 393 . 2 (((𝜑𝜓) ∨ (𝜑𝜒)) → (𝜑 ∧ (𝜓𝜒)))
93, 8impbii 199 1 ((𝜑 ∧ (𝜓𝜒)) ↔ ((𝜑𝜓) ∨ (𝜑𝜒)))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196   ∨ wo 382   ∧ wa 383 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 197  df-or 384  df-an 385 This theorem is referenced by:  andir  948  anddi  950  annotanannotOLD  978  cadan  1697  indi  4016  indifdir  4026  unrab  4041  unipr  4601  uniun  4608  unopab  4880  xpundi  5328  difxp  5716  coundir  5798  ordnbtwnOLD  5978  imadif  6134  unpreima  6504  tpostpos  7541  elznn0nn  11583  faclbnd4lem4  13277  opsrtoslem1  19686  mbfmax  23615  fta1glem2  24125  ofmulrt  24236  lgsquadlem3  25306  difrab2  29646  ordtconnlem1  30279  ballotlemodife  30868  subfacp1lem6  31474  soseq  32060  nosep1o  32138  lineunray  32560  bj-ismooredr2  33371  poimirlem30  33752  itg2addnclem2  33775  lzunuz  37833  diophun  37839  rmydioph  38083  rp-isfinite6  38366  relexpxpmin  38511  andi3or  38822  clsk1indlem3  38843  zeoALTV  42091
 Copyright terms: Public domain W3C validator