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  3952  disji2  4191  disjxiun  4201  pwssun  4481  swopo  4505  somo  4529  ordtri3or  4605  ordtri1  4606  ordtri3  4609  ord0eln0  4627  suc11  4677  elpwunsn  4749  ordeleqon  4761  ssonprc  4764  onmindif2  4784  limsssuc  4822  limom  4852  frsn  4940  foconst  5656  onfununi  6595  oeeulem  6836  uniinqs  6976  pw2f1olem  7204  pssnn  7319  ordtypelem9  7487  ordtypelem10  7488  oismo  7501  preleq  7564  suc11reg  7566  cantnfp1lem2  7627  cantnflem1  7637  cnfcom2lem  7650  cnfcom3lem  7652  rankxpsuc  7798  cardlim  7851  alephdom  7954  cardaleph  7962  iscard3  7966  pwcdadom  8088  cfslbn  8139  fin1a2lem12  8283  gchi  8491  fpwwe2lem13  8509  tskssel  8624  inttsk  8641  inar1  8642  r1tskina  8649  tskuni  8650  gruina  8685  grur1  8687  nlt1pi  8775  nqereu  8798  leltne  9156  nneo  10345  zeo2  10348  xrleltne  10730  nltpnft  10746  ngtmnft  10747  xrrebnd  10748  xaddf  10802  xrsupsslem  10877  xrinfmsslem  10878  seqf1olem1  11354  seqf1olem2  11355  discr1  11507  hashnncl  11637  seqcoll2  11705  sqeqd  11963  sqrmo  12049  isercoll  12453  dvdseq  12889  bitsfzo  12939  bitsinv1lem  12945  bitsf1  12950  bezoutlem3  13032  eucalglt  13068  phibndlem  13151  dfphi2  13155  prmdiv  13166  odzdvds  13173  pceq0  13236  pc2dvds  13244  fldivp1  13258  pcfac  13260  prmreclem3  13278  1arith  13287  4sqlem10  13307  4sqlem17  13321  4sqlem18  13322  vdwlem6  13346  ramubcl  13378  ramcl  13389  mrissmrcd  13857  oddvdsnn0  15174  odnncl  15175  oddvds  15177  odcl2  15193  gexdvds  15210  gexnnod  15214  sylow1lem1  15224  odcau  15230  pgpssslw  15240  efgs1b  15360  efgredlema  15364  torsubg  15461  prmcyg  15495  gsumval3eu  15505  ablfacrplem  15615  ablfac1eu  15623  lspdisj  16189  lspsncv0  16210  fidomndrnglem  16358  gzrngunitlem  16755  prmirredlem  16765  fctop  17060  cctop  17062  ppttop  17063  pptbas  17064  ordtrest2lem  17259  conclo  17470  txindis  17658  filcon  17907  ufilb  17930  cldsubg  18132  reconnlem1  18849  reconnlem2  18850  metds0  18872  metdseq0  18876  metnrmlem1a  18880  iccpnfhmeo  18962  xrhmeo  18963  cphsubrglem  19132  minveclem3b  19321  minveclem4a  19323  vitalilem4  19495  itg2gt0  19644  itgsplitioo  19721  limccnp2  19771  rollelem  19865  dvlip  19869  itgsubstlem  19924  plyaddlem1  20124  plymullem1  20125  coefv0  20158  dgreq0  20175  radcnv0  20324  pserdvlem2  20336  pilem2  20360  sineq0  20421  logtayl  20543  cxpsqr  20586  isosctrlem2  20655  atantayl2  20770  leibpilem1  20772  rlimcnp2  20797  amgm  20821  basellem3  20857  muval2  20909  sqf11  20914  ppinprm  20927  chtnprm  20929  perfectlem2  21006  lgsdir  21106  lgsabs1  21110  lgseisenlem1  21125  2sqlem7  21146  2sqblem  21153  chebbnd1lem1  21155  dchrisum0flblem1  21194  pntpbnd1  21272  pntpbnd2  21273  ostth  21325  minvecolem5  22375  staddi  23741  stadd3i  23743  atsseq  23842  atom1d  23848  atoml2i  23878  disji2f  24011  disjif2  24015  subfacp1lem6  24863  cvmscld  24952  cvmsss2  24953  cvmseu  24955  ordtoplem  26177  ordcmp  26189  heiborlem6  26516  isfldidl  26669  pridlc2  26673  ctbnfien  26870  pw2f1ocnv  27099  unxpwdom3  27224  dgrsub2  27307  psgnunilem5  27385  fmul01lt1lem1  27681  stoweidlem35  27751  stirlinglem5  27794  stirlinglem12  27801  lsatcmp  29738  lsatcmp2  29739  2atm  30261  trlatn0  30906  trlval3  30921  cdleme18c  31027  cdlemg17b  31396  cdlemg17i  31403  cdlemh  31551  dia2dimlem2  31800  dia2dimlem3  31801  dochlkr  32120  dochkrshp  32121  lcfl6  32235  lcfrlem9  32285  hdmap14lem6  32611  hgmapval0  32630
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