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  3928  disji2  4167  disjxiun  4177  pwssun  4457  swopo  4481  somo  4505  ordtri3or  4581  ordtri1  4582  ordtri3  4585  ord0eln0  4603  suc11  4652  elpwunsn  4724  ordeleqon  4736  ssonprc  4739  onmindif2  4759  limsssuc  4797  limom  4827  frsn  4915  foconst  5631  onfununi  6570  oeeulem  6811  uniinqs  6951  pw2f1olem  7179  pssnn  7294  ordtypelem9  7459  ordtypelem10  7460  oismo  7473  preleq  7536  suc11reg  7538  cantnfp1lem2  7599  cantnflem1  7609  cnfcom2lem  7622  cnfcom3lem  7624  rankxpsuc  7770  cardlim  7823  alephdom  7926  cardaleph  7934  iscard3  7938  pwcdadom  8060  cfslbn  8111  fin1a2lem12  8255  gchi  8463  fpwwe2lem13  8481  tskssel  8596  inttsk  8613  inar1  8614  r1tskina  8621  tskuni  8622  gruina  8657  grur1  8659  nlt1pi  8747  nqereu  8770  leltne  9128  nneo  10317  zeo2  10320  xrleltne  10702  nltpnft  10718  ngtmnft  10719  xrrebnd  10720  xaddf  10774  xrsupsslem  10849  xrinfmsslem  10850  seqf1olem1  11325  seqf1olem2  11326  discr1  11478  hashnncl  11608  seqcoll2  11676  sqeqd  11934  sqrmo  12020  isercoll  12424  dvdseq  12860  bitsfzo  12910  bitsinv1lem  12916  bitsf1  12921  bezoutlem3  13003  eucalglt  13039  phibndlem  13122  dfphi2  13126  prmdiv  13137  odzdvds  13144  pceq0  13207  pc2dvds  13215  fldivp1  13229  pcfac  13231  prmreclem3  13249  1arith  13258  4sqlem10  13278  4sqlem17  13292  4sqlem18  13293  vdwlem6  13317  ramubcl  13349  ramcl  13360  mrissmrcd  13828  oddvdsnn0  15145  odnncl  15146  oddvds  15148  odcl2  15164  gexdvds  15181  gexnnod  15185  sylow1lem1  15195  odcau  15201  pgpssslw  15211  efgs1b  15331  efgredlema  15335  torsubg  15432  prmcyg  15466  gsumval3eu  15476  ablfacrplem  15586  ablfac1eu  15594  lspdisj  16160  lspsncv0  16181  fidomndrnglem  16329  gzrngunitlem  16726  prmirredlem  16736  fctop  17031  cctop  17033  ppttop  17034  pptbas  17035  ordtrest2lem  17229  conclo  17439  txindis  17627  filcon  17876  ufilb  17899  cldsubg  18101  reconnlem1  18818  reconnlem2  18819  metds0  18841  metdseq0  18845  metnrmlem1a  18849  iccpnfhmeo  18931  xrhmeo  18932  cphsubrglem  19101  minveclem3b  19290  minveclem4a  19292  vitalilem4  19464  itg2gt0  19613  itgsplitioo  19690  limccnp2  19740  rollelem  19834  dvlip  19838  itgsubstlem  19893  plyaddlem1  20093  plymullem1  20094  coefv0  20127  dgreq0  20144  radcnv0  20293  pserdvlem2  20305  pilem2  20329  sineq0  20390  logtayl  20512  cxpsqr  20555  isosctrlem2  20624  atantayl2  20739  leibpilem1  20741  rlimcnp2  20766  amgm  20790  basellem3  20826  muval2  20878  sqf11  20883  ppinprm  20896  chtnprm  20898  perfectlem2  20975  lgsdir  21075  lgsabs1  21079  lgseisenlem1  21094  2sqlem7  21115  2sqblem  21122  chebbnd1lem1  21124  dchrisum0flblem1  21163  pntpbnd1  21241  pntpbnd2  21242  ostth  21294  minvecolem5  22344  staddi  23710  stadd3i  23712  atsseq  23811  atom1d  23817  atoml2i  23847  disji2f  23980  disjif2  23984  subfacp1lem6  24832  cvmscld  24921  cvmsss2  24922  cvmseu  24924  ordtoplem  26097  ordcmp  26109  heiborlem6  26423  isfldidl  26576  pridlc2  26580  ctbnfien  26777  pw2f1ocnv  27006  unxpwdom3  27132  dgrsub2  27215  psgnunilem5  27293  fmul01lt1lem1  27589  stoweidlem35  27659  stirlinglem5  27702  stirlinglem12  27709  lsatcmp  29498  lsatcmp2  29499  2atm  30021  trlatn0  30666  trlval3  30681  cdleme18c  30787  cdlemg17b  31156  cdlemg17i  31163  cdlemh  31311  dia2dimlem2  31560  dia2dimlem3  31561  dochlkr  31880  dochkrshp  31881  lcfl6  31995  lcfrlem9  32045  hdmap14lem6  32371  hgmapval0  32390
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