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

Theorem ord 377
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 370 . 2  |-  ( ( ps  \/  ch )  <->  ( -.  ps  ->  ch ) )
31, 2sylib 196 1  |-  ( ph  ->  ( -.  ps  ->  ch ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 368
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 185  df-or 370
This theorem is referenced by:  ornld  896  orcanai  911  oplem1  962  ecase23d  1332  19.33b  1673  elpwunsn  4068  eqsn  4188  disji2  4434  disjxiun  4444  pwssun  4786  swopo  4810  somo  4834  ordtri3or  4910  ordtri1  4911  ordtri3  4914  ord0eln0  4932  suc11  4981  frsn  5070  foconst  5806  ordeleqon  6608  ssonprc  6611  onmindif2  6631  limsssuc  6669  limom  6699  onfununi  7012  oeeulem  7250  uniinqs  7391  pw2f1olem  7621  pssnn  7738  ordtypelem9  7951  ordtypelem10  7952  oismo  7965  preleq  8034  suc11reg  8036  cantnfp1lem2  8098  cantnflem1  8108  cantnfp1lem2OLD  8124  cantnflem1OLD  8131  cnfcom2lem  8145  cnfcom3lem  8147  cnfcom2lemOLD  8153  cnfcom3lemOLD  8155  rankxpsuc  8300  cardlim  8353  alephdom  8462  cardaleph  8470  iscard3  8474  pwcdadom  8596  cfslbn  8647  fin1a2lem12  8791  gchi  9002  fpwwe2lem13  9020  tskssel  9135  inttsk  9152  inar1  9153  r1tskina  9160  tskuni  9161  gruina  9196  grur1  9198  nlt1pi  9284  nqereu  9307  leltne  9674  nneo  10944  zeo2  10947  xrleltne  11351  nltpnft  11367  ngtmnft  11368  xrrebnd  11369  xaddf  11423  xrsupsslem  11498  xrinfmsslem  11499  seqf1olem1  12114  seqf1olem2  12115  discr1  12270  hashnncl  12404  seqcoll2  12479  sqeqd  12962  sqrmo  13048  isercoll  13453  dvdseq  13892  bitsfzo  13944  bitsinv1lem  13950  bitsf1  13955  bezoutlem3  14037  eucalglt  14073  phibndlem  14159  dfphi2  14163  prmdiv  14174  odzdvds  14181  pceq0  14253  pc2dvds  14261  fldivp1  14275  pcfac  14277  prmreclem3  14295  1arith  14304  4sqlem10  14324  4sqlem17  14338  4sqlem18  14339  vdwlem6  14363  ramubcl  14395  ramcl  14406  mrissmrcd  14895  psgnunilem5  16325  oddvdsnn0  16374  odnncl  16375  oddvds  16377  odcl2  16393  gexdvds  16410  gexnnod  16414  sylow1lem1  16424  odcau  16430  pgpssslw  16440  efgs1b  16560  efgredlema  16564  torsubg  16663  prmcyg  16699  gsumval3eu  16710  ablfacrplem  16918  ablfac1eu  16926  lspdisj  17571  lspsncv0  17592  fidomndrnglem  17754  gzrngunitlem  18278  prmirredlem  18318  prmirredlemOLD  18321  fctop  19299  cctop  19301  ppttop  19302  pptbas  19303  ordtrest2lem  19498  conclo  19710  txindis  19898  filcon  20147  ufilb  20170  cldsubg  20372  reconnlem1  21094  reconnlem2  21095  metds0  21117  metdseq0  21121  metnrmlem1a  21125  iccpnfhmeo  21208  xrhmeo  21209  cphsubrglem  21387  minveclem3b  21606  minveclem4a  21608  vitalilem4  21783  itg2gt0  21930  itgsplitioo  22007  limccnp2  22059  rollelem  22153  dvlip  22157  itgsubstlem  22212  plyaddlem1  22373  plymullem1  22374  coefv0  22407  dgreq0  22424  radcnv0  22573  pserdvlem2  22585  pilem2  22609  sineq0  22675  logtayl  22797  cxpsqrt  22840  isosctrlem2  22909  atantayl2  23025  leibpilem1  23027  rlimcnp2  23052  amgm  23076  basellem3  23112  muval2  23164  sqf11  23169  ppinprm  23182  chtnprm  23184  perfectlem2  23261  lgsdir  23361  lgsabs1  23365  lgseisenlem1  23380  2sqlem7  23401  2sqblem  23408  chebbnd1lem1  23410  dchrisum0flblem1  23449  pntpbnd1  23527  pntpbnd2  23528  ostth  23580  coltr2  23769  colmid  23801  symquadlem  23802  midexlem  23805  colperp  23836  mideu  23842  lmieu  23855  lmicom  23859  lmiisolem  23866  minvecolem5  25501  staddi  26869  stadd3i  26871  atsseq  26970  atom1d  26976  atoml2i  27006  disji2f  27139  disjif2  27143  ordtrest2NEWlem  27568  eulerpartlemb  27975  subfacp1lem6  28297  cvmscld  28386  cvmsss2  28387  cvmseu  28389  ordtoplem  29505  ordcmp  29517  heiborlem6  29943  isfldidl  30096  pridlc2  30100  mpt2bi123f  30203  mptbi12f  30207  ac6s6  30212  ctbnfien  30384  pw2f1ocnv  30611  unxpwdom3  30673  dgrsub2  30716  fmul01lt1lem1  31162  stoweidlem35  31363  stirlinglem5  31406  stirlinglem12  31413  fourierdlem42  31477  lsatcmp  33818  lsatcmp2  33819  2atm  34341  trlatn0  34986  trlval3  35001  cdleme18c  35107  cdlemg17b  35476  cdlemg17i  35483  cdlemh  35631  dia2dimlem2  35880  dia2dimlem3  35881  dochlkr  36200  dochkrshp  36201  lcfl6  36315  lcfrlem9  36365  hdmap14lem6  36691  hgmapval0  36710
  Copyright terms: Public domain W3C validator