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

Theorem ord 367
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 360 . 2  |-  ( ( ps  \/  ch )  <->  ( -.  ps  ->  ch ) )
31, 2sylib 189 1  |-  ( ph  ->  ( -.  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 358
This theorem is referenced by:  orcanai  880  oplem1  931  ecase23d  1287  19.33b  1618  eqsn  3960  disji2  4199  disjxiun  4209  pwssun  4489  swopo  4513  somo  4537  ordtri3or  4613  ordtri1  4614  ordtri3  4617  ord0eln0  4635  suc11  4685  elpwunsn  4757  ordeleqon  4769  ssonprc  4772  onmindif2  4792  limsssuc  4830  limom  4860  frsn  4948  foconst  5664  onfununi  6603  oeeulem  6844  uniinqs  6984  pw2f1olem  7212  pssnn  7327  ordtypelem9  7495  ordtypelem10  7496  oismo  7509  preleq  7572  suc11reg  7574  cantnfp1lem2  7635  cantnflem1  7645  cnfcom2lem  7658  cnfcom3lem  7660  rankxpsuc  7806  cardlim  7859  alephdom  7962  cardaleph  7970  iscard3  7974  pwcdadom  8096  cfslbn  8147  fin1a2lem12  8291  gchi  8499  fpwwe2lem13  8517  tskssel  8632  inttsk  8649  inar1  8650  r1tskina  8657  tskuni  8658  gruina  8693  grur1  8695  nlt1pi  8783  nqereu  8806  leltne  9164  nneo  10353  zeo2  10356  xrleltne  10738  nltpnft  10754  ngtmnft  10755  xrrebnd  10756  xaddf  10810  xrsupsslem  10885  xrinfmsslem  10886  seqf1olem1  11362  seqf1olem2  11363  discr1  11515  hashnncl  11645  seqcoll2  11713  sqeqd  11971  sqrmo  12057  isercoll  12461  dvdseq  12897  bitsfzo  12947  bitsinv1lem  12953  bitsf1  12958  bezoutlem3  13040  eucalglt  13076  phibndlem  13159  dfphi2  13163  prmdiv  13174  odzdvds  13181  pceq0  13244  pc2dvds  13252  fldivp1  13266  pcfac  13268  prmreclem3  13286  1arith  13295  4sqlem10  13315  4sqlem17  13329  4sqlem18  13330  vdwlem6  13354  ramubcl  13386  ramcl  13397  mrissmrcd  13865  oddvdsnn0  15182  odnncl  15183  oddvds  15185  odcl2  15201  gexdvds  15218  gexnnod  15222  sylow1lem1  15232  odcau  15238  pgpssslw  15248  efgs1b  15368  efgredlema  15372  torsubg  15469  prmcyg  15503  gsumval3eu  15513  ablfacrplem  15623  ablfac1eu  15631  lspdisj  16197  lspsncv0  16218  fidomndrnglem  16366  gzrngunitlem  16763  prmirredlem  16773  fctop  17068  cctop  17070  ppttop  17071  pptbas  17072  ordtrest2lem  17267  conclo  17478  txindis  17666  filcon  17915  ufilb  17938  cldsubg  18140  reconnlem1  18857  reconnlem2  18858  metds0  18880  metdseq0  18884  metnrmlem1a  18888  iccpnfhmeo  18970  xrhmeo  18971  cphsubrglem  19140  minveclem3b  19329  minveclem4a  19331  vitalilem4  19503  itg2gt0  19652  itgsplitioo  19729  limccnp2  19779  rollelem  19873  dvlip  19877  itgsubstlem  19932  plyaddlem1  20132  plymullem1  20133  coefv0  20166  dgreq0  20183  radcnv0  20332  pserdvlem2  20344  pilem2  20368  sineq0  20429  logtayl  20551  cxpsqr  20594  isosctrlem2  20663  atantayl2  20778  leibpilem1  20780  rlimcnp2  20805  amgm  20829  basellem3  20865  muval2  20917  sqf11  20922  ppinprm  20935  chtnprm  20937  perfectlem2  21014  lgsdir  21114  lgsabs1  21118  lgseisenlem1  21133  2sqlem7  21154  2sqblem  21161  chebbnd1lem1  21163  dchrisum0flblem1  21202  pntpbnd1  21280  pntpbnd2  21281  ostth  21333  minvecolem5  22383  staddi  23749  stadd3i  23751  atsseq  23850  atom1d  23856  atoml2i  23886  disji2f  24019  disjif2  24023  subfacp1lem6  24871  cvmscld  24960  cvmsss2  24961  cvmseu  24963  ordtoplem  26185  ordcmp  26197  heiborlem6  26525  isfldidl  26678  pridlc2  26682  ctbnfien  26879  pw2f1ocnv  27108  unxpwdom3  27233  dgrsub2  27316  psgnunilem5  27394  fmul01lt1lem1  27690  stoweidlem35  27760  stirlinglem5  27803  stirlinglem12  27810  lsatcmp  29801  lsatcmp2  29802  2atm  30324  trlatn0  30969  trlval3  30984  cdleme18c  31090  cdlemg17b  31459  cdlemg17i  31466  cdlemh  31614  dia2dimlem2  31863  dia2dimlem3  31864  dochlkr  32183  dochkrshp  32184  lcfl6  32298  lcfrlem9  32348  hdmap14lem6  32674  hgmapval0  32693
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 178  df-or 360
  Copyright terms: Public domain W3C validator