MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ord 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  1615  eqsn  3905  disji2  4142  disjxiun  4152  pwssun  4432  swopo  4456  somo  4480  ordtri3or  4556  ordtri1  4557  ordtri3  4560  ord0eln0  4578  suc11  4627  elpwunsn  4699  ordeleqon  4711  ssonprc  4714  onmindif2  4734  limsssuc  4772  limom  4802  frsn  4890  foconst  5606  onfununi  6541  oeeulem  6782  uniinqs  6922  pw2f1olem  7150  pssnn  7265  ordtypelem9  7430  ordtypelem10  7431  oismo  7444  preleq  7507  suc11reg  7509  cantnfp1lem2  7570  cantnflem1  7580  cnfcom2lem  7593  cnfcom3lem  7595  rankxpsuc  7741  cardlim  7794  alephdom  7897  cardaleph  7905  iscard3  7909  pwcdadom  8031  cfslbn  8082  fin1a2lem12  8226  gchi  8434  fpwwe2lem13  8452  tskssel  8567  inttsk  8584  inar1  8585  r1tskina  8592  tskuni  8593  gruina  8628  grur1  8630  nlt1pi  8718  nqereu  8741  leltne  9099  nneo  10287  zeo2  10290  xrleltne  10672  nltpnft  10688  ngtmnft  10689  xrrebnd  10690  xaddf  10744  xrsupsslem  10819  xrinfmsslem  10820  seqf1olem1  11291  seqf1olem2  11292  discr1  11444  hashnncl  11574  seqcoll2  11642  sqeqd  11900  sqrmo  11986  isercoll  12390  dvdseq  12826  bitsfzo  12876  bitsinv1lem  12882  bitsf1  12887  bezoutlem3  12969  eucalglt  13005  phibndlem  13088  dfphi2  13092  prmdiv  13103  odzdvds  13110  pceq0  13173  pc2dvds  13181  fldivp1  13195  pcfac  13197  prmreclem3  13215  1arith  13224  4sqlem10  13244  4sqlem17  13258  4sqlem18  13259  vdwlem6  13283  ramubcl  13315  ramcl  13326  mrissmrcd  13794  oddvdsnn0  15111  odnncl  15112  oddvds  15114  odcl2  15130  gexdvds  15147  gexnnod  15151  sylow1lem1  15161  odcau  15167  pgpssslw  15177  efgs1b  15297  efgredlema  15301  torsubg  15398  prmcyg  15432  gsumval3eu  15442  ablfacrplem  15552  ablfac1eu  15560  lspdisj  16126  lspsncv0  16147  fidomndrnglem  16295  gzrngunitlem  16688  prmirredlem  16698  fctop  16993  cctop  16995  ppttop  16996  pptbas  16997  ordtrest2lem  17191  conclo  17401  txindis  17589  filcon  17838  ufilb  17861  cldsubg  18063  reconnlem1  18730  reconnlem2  18731  metds0  18753  metdseq0  18757  metnrmlem1a  18761  iccpnfhmeo  18843  xrhmeo  18844  cphsubrglem  19013  minveclem3b  19198  minveclem4a  19200  vitalilem4  19372  itg2gt0  19521  itgsplitioo  19598  limccnp2  19648  rollelem  19742  dvlip  19746  itgsubstlem  19801  plyaddlem1  20001  plymullem1  20002  coefv0  20035  dgreq0  20052  radcnv0  20201  pserdvlem2  20213  pilem2  20237  sineq0  20298  logtayl  20420  cxpsqr  20463  isosctrlem2  20532  atantayl2  20647  leibpilem1  20649  rlimcnp2  20674  amgm  20698  basellem3  20734  muval2  20786  sqf11  20791  ppinprm  20804  chtnprm  20806  perfectlem2  20883  lgsdir  20983  lgsabs1  20987  lgseisenlem1  21002  2sqlem7  21023  2sqblem  21030  chebbnd1lem1  21032  dchrisum0flblem1  21071  pntpbnd1  21149  pntpbnd2  21150  ostth  21202  minvecolem5  22233  staddi  23599  stadd3i  23601  atsseq  23700  atom1d  23706  atoml2i  23736  disji2f  23865  disjif2  23869  subfacp1lem6  24652  cvmscld  24741  cvmsss2  24742  cvmseu  24744  ordtoplem  25901  ordcmp  25913  heiborlem6  26218  isfldidl  26371  pridlc2  26375  ctbnfien  26572  pw2f1ocnv  26801  unxpwdom3  26927  dgrsub2  27010  psgnunilem5  27088  fmul01lt1lem1  27384  stoweidlem35  27454  stirlinglem5  27497  stirlinglem12  27504  lsatcmp  29120  lsatcmp2  29121  2atm  29643  trlatn0  30288  trlval3  30303  cdleme18c  30409  cdlemg17b  30778  cdlemg17i  30785  cdlemh  30933  dia2dimlem2  31182  dia2dimlem3  31183  dochlkr  31502  dochkrshp  31503  lcfl6  31617  lcfrlem9  31667  hdmap14lem6  31993  hgmapval0  32012
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