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  1286  19.33b  1613  eqsn  3875  disji2  4112  disjxiun  4122  pwssun  4402  swopo  4427  somo  4451  ordtri3or  4527  ordtri1  4528  ordtri3  4531  ord0eln0  4549  suc11  4599  elpwunsn  4671  ordeleqon  4683  ssonprc  4686  onmindif2  4706  limsssuc  4744  limom  4774  frsn  4863  foconst  5568  onfununi  6500  oeeulem  6741  uniinqs  6881  pw2f1olem  7109  pssnn  7224  ordtypelem9  7388  ordtypelem10  7389  oismo  7402  preleq  7465  suc11reg  7467  cantnfp1lem2  7528  cantnflem1  7538  cnfcom2lem  7551  cnfcom3lem  7553  rankxpsuc  7699  cardlim  7752  alephdom  7855  cardaleph  7863  iscard3  7867  pwcdadom  7989  cfslbn  8040  fin1a2lem12  8184  gchi  8393  fpwwe2lem13  8411  tskssel  8526  inttsk  8543  inar1  8544  r1tskina  8551  tskuni  8552  gruina  8587  grur1  8589  nlt1pi  8677  nqereu  8700  leltne  9058  nneo  10246  zeo2  10249  xrleltne  10631  nltpnft  10647  ngtmnft  10648  xrrebnd  10649  xaddf  10703  xrsupsslem  10778  xrinfmsslem  10779  seqf1olem1  11249  seqf1olem2  11250  discr1  11402  hashnncl  11532  seqcoll2  11600  sqeqd  11858  sqrmo  11944  isercoll  12348  dvdseq  12784  bitsfzo  12834  bitsinv1lem  12840  bitsf1  12845  bezoutlem3  12927  eucalglt  12963  phibndlem  13046  dfphi2  13050  prmdiv  13061  odzdvds  13068  pceq0  13131  pc2dvds  13139  fldivp1  13153  pcfac  13155  prmreclem3  13173  1arith  13182  4sqlem10  13202  4sqlem17  13216  4sqlem18  13217  vdwlem6  13241  ramubcl  13273  ramcl  13284  mrissmrcd  13752  oddvdsnn0  15069  odnncl  15070  oddvds  15072  odcl2  15088  gexdvds  15105  gexnnod  15109  sylow1lem1  15119  odcau  15125  pgpssslw  15135  efgs1b  15255  efgredlema  15259  torsubg  15356  prmcyg  15390  gsumval3eu  15400  ablfacrplem  15510  ablfac1eu  15518  lspdisj  16088  lspsncv0  16109  fidomndrnglem  16257  gzrngunitlem  16653  prmirredlem  16663  fctop  16958  cctop  16960  ppttop  16961  pptbas  16962  ordtrest2lem  17150  conclo  17358  txindis  17545  filcon  17791  ufilb  17814  cldsubg  18006  reconnlem1  18545  reconnlem2  18546  metds0  18568  metdseq0  18572  metnrmlem1a  18576  iccpnfhmeo  18658  xrhmeo  18659  cphsubrglem  18828  minveclem3b  19007  minveclem4a  19009  vitalilem4  19181  itg2gt0  19330  itgsplitioo  19407  limccnp2  19457  rollelem  19551  dvlip  19555  itgsubstlem  19610  plyaddlem1  19810  plymullem1  19811  coefv0  19844  dgreq0  19861  radcnv0  20010  pserdvlem2  20022  pilem2  20046  sineq0  20107  logtayl  20229  cxpsqr  20272  isosctrlem2  20341  atantayl2  20456  leibpilem1  20458  rlimcnp2  20483  amgm  20507  basellem3  20543  muval2  20595  sqf11  20600  ppinprm  20613  chtnprm  20615  perfectlem2  20692  lgsdir  20792  lgsabs1  20796  lgseisenlem1  20811  2sqlem7  20832  2sqblem  20839  chebbnd1lem1  20841  dchrisum0flblem1  20880  pntpbnd1  20958  pntpbnd2  20959  ostth  21011  minvecolem5  21773  staddi  23139  stadd3i  23141  atsseq  23240  atom1d  23246  atoml2i  23276  elpreq  23397  disji2f  23417  disjif2  23421  subfacp1lem6  24319  cvmscld  24407  cvmsss2  24408  cvmseu  24410  ordtoplem  25616  ordcmp  25628  heiborlem6  26046  isfldidl  26199  pridlc2  26203  ctbnfien  26407  pw2f1ocnv  26636  unxpwdom3  26762  dgrsub2  26845  psgnunilem5  26923  stirlinglem5  27333  stirlinglem12  27340  lsatcmp  29264  lsatcmp2  29265  2atm  29787  trlatn0  30432  trlval3  30447  cdleme18c  30553  cdlemg17b  30922  cdlemg17i  30929  cdlemh  31077  dia2dimlem2  31326  dia2dimlem3  31327  dochlkr  31646  dochkrshp  31647  lcfl6  31761  lcfrlem9  31811  hdmap14lem6  32137  hgmapval0  32156
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