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

Theorem andi 1010
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 868 . . 3 ((𝜑𝜓) → ((𝜑𝜓) ∨ (𝜑𝜒)))
2 olc 869 . . 3 ((𝜑𝜒) → ((𝜑𝜓) ∨ (𝜑𝜒)))
31, 2jaodan 960 . 2 ((𝜑 ∧ (𝜓𝜒)) → ((𝜑𝜓) ∨ (𝜑𝜒)))
4 orc 868 . . . 4 (𝜓 → (𝜓𝜒))
54anim2i 617 . . 3 ((𝜑𝜓) → (𝜑 ∧ (𝜓𝜒)))
6 olc 869 . . . 4 (𝜒 → (𝜓𝜒))
76anim2i 617 . . 3 ((𝜑𝜒) → (𝜑 ∧ (𝜓𝜒)))
85, 7jaoi 858 . 2 (((𝜑𝜓) ∨ (𝜑𝜒)) → (𝜑 ∧ (𝜓𝜒)))
93, 8impbii 209 1 ((𝜑 ∧ (𝜓𝜒)) ↔ ((𝜑𝜓) ∨ (𝜑𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395  wo 848
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 207  df-an 396  df-or 849
This theorem is referenced by:  andir  1011  anddi  1013  cadan  1609  indi  4284  unrab  4315  uniun  4930  unopab  5224  xpundi  5754  difxp  6184  coundir  6268  imadif  6650  unpreima  7083  soseq  8184  tpostpos  8271  elznn0nn  12627  faclbnd4lem4  14335  opsrtoslem1  22079  mbfmax  25684  fta1glem2  26208  ofmulrt  26323  lgsquadlem3  27426  nogesgn1o  27718  nosep1o  27726  noinfbnd2lem1  27775  difrab2  32517  ordtconnlem1  33923  ballotlemodife  34500  subfacp1lem6  35190  satf0op  35382  lineunray  36148  wl-ifpimpr  37467  wl-df2-3mintru2  37486  poimirlem30  37657  itg2addnclem2  37679  sticksstones22  42169  lzunuz  42779  diophun  42784  rmydioph  43026  fzunt  43468  fzuntd  43469  fzunt1d  43470  fzuntgd  43471  rp-isfinite6  43531  relexpxpmin  43730  andi3or  44037  clsk1indlem3  44056  simpcntrab  46885  zeoALTV  47657
  Copyright terms: Public domain W3C validator