MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ord Unicode version

Theorem ord 366
Description: Deduce implication from disjunction. (Contributed by NM, 18-May-1994.)
Hypothesis
Ref Expression
ord.1  |-  ( ph  ->  ( ps  \/  ch ) )
Assertion
Ref Expression
ord  |-  ( ph  ->  ( -.  ps  ->  ch ) )

Proof of Theorem ord
StepHypRef Expression
1 ord.1 . 2  |-  ( ph  ->  ( ps  \/  ch ) )
2 df-or 359 . 2  |-  ( ( ps  \/  ch )  <->  ( -.  ps  ->  ch ) )
31, 2sylib 188 1  |-  ( ph  ->  ( -.  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 357
This theorem is referenced by:  orcanai  879  oplem1  930  ecase23d  1285  19.33b  1595  eqsn  3775  disji2  4010  disjxiun  4020  pwssun  4299  swopo  4324  somo  4348  ordtri3or  4424  ordtri1  4425  ordtri3  4428  ord0eln0  4446  suc11  4496  elpwunsn  4568  ordeleqon  4580  ssonprc  4583  onmindif2  4603  limsssuc  4641  limom  4671  frsn  4760  foconst  5462  onfununi  6358  oeeulem  6599  pw2f1olem  6966  pssnn  7081  ordtypelem9  7241  ordtypelem10  7242  oismo  7255  preleq  7318  suc11reg  7320  cantnfp1lem2  7381  cantnflem1  7391  cnfcom2lem  7404  cnfcom3lem  7406  rankxpsuc  7552  cardlim  7605  alephdom  7708  cardaleph  7716  iscard3  7720  pwcdadom  7842  cfslbn  7893  fin1a2lem12  8037  gchi  8246  fpwwe2lem13  8264  tskssel  8379  inttsk  8396  inar1  8397  r1tskina  8404  tskuni  8405  gruina  8440  grur1  8442  nlt1pi  8530  nqereu  8553  leltne  8911  nneo  10095  zeo2  10098  xrleltne  10479  nltpnft  10495  ngtmnft  10496  xrrebnd  10497  xaddf  10551  xrsupsslem  10625  xrinfmsslem  10626  seqf1olem1  11085  seqf1olem2  11086  discr1  11237  hashnncl  11354  seqcoll2  11402  sqeqd  11651  sqrmo  11737  isercoll  12141  dvdseq  12576  bitsfzo  12626  bitsinv1lem  12632  bitsf1  12637  bezoutlem3  12719  eucalglt  12755  phibndlem  12838  dfphi2  12842  prmdiv  12853  odzdvds  12860  pceq0  12923  pc2dvds  12931  fldivp1  12945  pcfac  12947  prmreclem3  12965  1arith  12974  4sqlem10  12994  4sqlem17  13008  4sqlem18  13009  vdwlem6  13033  ramubcl  13065  ramcl  13076  mrissmrcd  13542  oddvdsnn0  14859  odnncl  14860  oddvds  14862  odcl2  14878  gexdvds  14895  gexnnod  14899  sylow1lem1  14909  odcau  14915  pgpssslw  14925  efgs1b  15045  efgredlema  15049  torsubg  15146  prmcyg  15180  gsumval3eu  15190  ablfacrplem  15300  ablfac1eu  15308  lspdisj  15878  lspsncv0  15899  fidomndrnglem  16047  gzrngunitlem  16436  prmirredlem  16446  fctop  16741  cctop  16743  ppttop  16744  pptbas  16745  ordtrest2lem  16933  conclo  17141  txindis  17328  filcon  17578  ufilb  17601  cldsubg  17793  reconnlem1  18331  reconnlem2  18332  metds0  18354  metdseq0  18358  metnrmlem1a  18362  iccpnfhmeo  18443  xrhmeo  18444  cphsubrglem  18613  minveclem3b  18792  minveclem4a  18794  vitalilem4  18966  itg2gt0  19115  itgsplitioo  19192  limccnp2  19242  rollelem  19336  dvlip  19340  itgsubstlem  19395  plyaddlem1  19595  plymullem1  19596  coefv0  19629  dgreq0  19646  radcnv0  19792  pserdvlem2  19804  pilem2  19828  sineq0  19889  logtayl  20007  cxpsqr  20050  isosctrlem2  20119  atantayl2  20234  leibpilem1  20236  rlimcnp2  20261  amgm  20285  basellem3  20320  muval2  20372  sqf11  20377  ppinprm  20390  chtnprm  20392  perfectlem2  20469  lgsdir  20569  lgsabs1  20573  lgseisenlem1  20588  2sqlem7  20609  2sqblem  20616  chebbnd1lem1  20618  dchrisum0flblem1  20657  pntpbnd1  20735  pntpbnd2  20736  ostth  20788  minvecolem5  21460  staddi  22826  stadd3i  22828  atsseq  22927  atom1d  22933  atoml2i  22963  elpreq  23188  disji2f  23354  disjif2  23358  subfacp1lem6  23716  cvmscld  23804  cvmsss2  23805  cvmseu  23807  ordtoplem  24874  ordcmp  24886  nopsthph  24995  uninqs  25039  heiborlem6  26540  isfldidl  26693  pridlc2  26697  ctbnfien  26901  pw2f1ocnv  27130  unxpwdom3  27256  dgrsub2  27339  psgnunilem5  27417  stirlinglem5  27827  stirlinglem12  27834  lsatcmp  29193  lsatcmp2  29194  2atm  29716  trlatn0  30361  trlval3  30376  cdleme18c  30482  cdlemg17b  30851  cdlemg17i  30858  cdlemh  31006  dia2dimlem2  31255  dia2dimlem3  31256  dochlkr  31575  dochkrshp  31576  lcfl6  31690  lcfrlem9  31740  hdmap14lem6  32066  hgmapval0  32085
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-or 359
  Copyright terms: Public domain W3C validator