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

Theorem orrd 392
Description: Deduce disjunction from implication. (Contributed by NM, 27-Nov-1995.)
Hypothesis
Ref Expression
orrd.1 (𝜑 → (¬ 𝜓𝜒))
Assertion
Ref Expression
orrd (𝜑 → (𝜓𝜒))

Proof of Theorem orrd
StepHypRef Expression
1 orrd.1 . 2 (𝜑 → (¬ 𝜓𝜒))
2 pm2.54 388 . 2 ((¬ 𝜓𝜒) → (𝜓𝜒))
31, 2syl 17 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 382
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
This theorem is referenced by:  olc  398  orc  399  pm2.68  425  pm4.79  606  19.30  1849  axi12  2629  axbnd  2630  sspss  3739  eqoreldif  4257  pwpw0  4376  sssn  4390  pwsnALT  4461  unissint  4533  disjiund  4675  disjxiun  4681  disjxiunOLD  4682  otsndisj  5008  otiunsndisj  5009  pwssun  5049  isso2i  5096  ordtr3  5807  ordtr3OLD  5808  ordtri2or  5860  unizlim  5882  fvclss  6540  orduniorsuc  7072  ordzsl  7087  nn0suc  7132  xpexr  7148  odi  7704  swoso  7820  erdisj  7837  ordtypelem7  8470  wemapsolem  8496  domwdom  8520  iscard3  8954  ackbij1lem18  9097  fin56  9253  entric  9417  gchdomtri  9489  inttsk  9634  r1tskina  9642  psslinpr  9891  ssxr  10145  letric  10175  mul0or  10705  mulge0b  10931  zeo  11501  uzm1  11756  xrletri  12022  supxrgtmnf  12197  sq01  13026  ruclem3  15006  prm2orodd  15451  phiprmpw  15528  pleval2i  17011  irredn0  18749  drngmul0or  18816  lvecvs0or  19156  lssvs0or  19158  lspsnat  19193  lsppratlem1  19195  domnchr  19928  fctop  20856  cctop  20858  ppttop  20859  clslp  21000  restntr  21034  cnconn  21273  txindis  21485  txconn  21540  isufil2  21759  ufprim  21760  alexsubALTlem3  21900  pmltpc  23265  iundisj2  23363  limcco  23702  fta1b  23974  aalioulem2  24133  abelthlem2  24231  logreclem  24545  dchrfi  25025  2sqb  25202  tgbtwnconn1  25515  legov3  25538  coltr  25587  colline  25589  tglowdim2ln  25591  ragflat3  25646  ragperp  25657  lmieu  25721  lmicom  25725  lmimid  25731  numedglnl  26084  nvmul0or  27633  hvmul0or  28010  atomli  29369  atordi  29371  iundisj2f  29529  iundisj2fi  29684  signsply0  30756  cvmsdisj  31378  nepss  31725  dfon2lem6  31817  soseq  31879  nosepdmlem  31958  noetalem3  31990  btwnconn1lem13  32331  wl-exeq  33451  lsator0sp  34606  lkreqN  34775  2at0mat0  35129  trlator0  35776  dochkrshp4  36995  dochsat0  37063  lcfl6  37106  rp-fakeimass  38174  frege124d  38370  clsk1independent  38661  pm10.57  38887  icccncfext  40418  fourierdlem70  40711  uzlidlring  42254  nneop  42645
  Copyright terms: Public domain W3C validator