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  1285  19.33b  1597  eqsn  3777  disji2  4012  disjxiun  4022  pwssun  4301  swopo  4326  somo  4350  ordtri3or  4426  ordtri1  4427  ordtri3  4430  ord0eln0  4448  suc11  4498  elpwunsn  4570  ordeleqon  4582  ssonprc  4585  onmindif2  4605  limsssuc  4643  limom  4673  frsn  4762  foconst  5464  onfununi  6360  oeeulem  6601  pw2f1olem  6968  pssnn  7083  ordtypelem9  7243  ordtypelem10  7244  oismo  7257  preleq  7320  suc11reg  7322  cantnfp1lem2  7383  cantnflem1  7393  cnfcom2lem  7406  cnfcom3lem  7408  rankxpsuc  7554  cardlim  7607  alephdom  7710  cardaleph  7718  iscard3  7722  pwcdadom  7844  cfslbn  7895  fin1a2lem12  8039  gchi  8248  fpwwe2lem13  8266  tskssel  8381  inttsk  8398  inar1  8399  r1tskina  8406  tskuni  8407  gruina  8442  grur1  8444  nlt1pi  8532  nqereu  8555  leltne  8913  nneo  10097  zeo2  10100  xrleltne  10481  nltpnft  10497  ngtmnft  10498  xrrebnd  10499  xaddf  10553  xrsupsslem  10627  xrinfmsslem  10628  seqf1olem1  11087  seqf1olem2  11088  discr1  11239  hashnncl  11356  seqcoll2  11404  sqeqd  11653  sqrmo  11739  isercoll  12143  dvdseq  12578  bitsfzo  12628  bitsinv1lem  12634  bitsf1  12639  bezoutlem3  12721  eucalglt  12757  phibndlem  12840  dfphi2  12844  prmdiv  12855  odzdvds  12862  pceq0  12925  pc2dvds  12933  fldivp1  12947  pcfac  12949  prmreclem3  12967  1arith  12976  4sqlem10  12996  4sqlem17  13010  4sqlem18  13011  vdwlem6  13035  ramubcl  13067  ramcl  13078  mrissmrcd  13544  oddvdsnn0  14861  odnncl  14862  oddvds  14864  odcl2  14880  gexdvds  14897  gexnnod  14901  sylow1lem1  14911  odcau  14917  pgpssslw  14927  efgs1b  15047  efgredlema  15051  torsubg  15148  prmcyg  15182  gsumval3eu  15192  ablfacrplem  15302  ablfac1eu  15310  lspdisj  15880  lspsncv0  15901  fidomndrnglem  16049  gzrngunitlem  16438  prmirredlem  16448  fctop  16743  cctop  16745  ppttop  16746  pptbas  16747  ordtrest2lem  16935  conclo  17143  txindis  17330  filcon  17580  ufilb  17603  cldsubg  17795  reconnlem1  18333  reconnlem2  18334  metds0  18356  metdseq0  18360  metnrmlem1a  18364  iccpnfhmeo  18445  xrhmeo  18446  cphsubrglem  18615  minveclem3b  18794  minveclem4a  18796  vitalilem4  18968  itg2gt0  19117  itgsplitioo  19194  limccnp2  19244  rollelem  19338  dvlip  19342  itgsubstlem  19397  plyaddlem1  19597  plymullem1  19598  coefv0  19631  dgreq0  19648  radcnv0  19794  pserdvlem2  19806  pilem2  19830  sineq0  19891  logtayl  20009  cxpsqr  20052  isosctrlem2  20121  atantayl2  20236  leibpilem1  20238  rlimcnp2  20263  amgm  20287  basellem3  20322  muval2  20374  sqf11  20379  ppinprm  20392  chtnprm  20394  perfectlem2  20471  lgsdir  20571  lgsabs1  20575  lgseisenlem1  20590  2sqlem7  20611  2sqblem  20618  chebbnd1lem1  20620  dchrisum0flblem1  20659  pntpbnd1  20737  pntpbnd2  20738  ostth  20790  minvecolem5  21462  staddi  22828  stadd3i  22830  atsseq  22929  atom1d  22935  atoml2i  22965  elpreq  23190  disji2f  23356  disjif2  23360  subfacp1lem6  23718  cvmscld  23806  cvmsss2  23807  cvmseu  23809  ordtoplem  24876  ordcmp  24888  nopsthph  25006  uninqs  25050  heiborlem6  26551  isfldidl  26704  pridlc2  26708  ctbnfien  26912  pw2f1ocnv  27141  unxpwdom3  27267  dgrsub2  27350  psgnunilem5  27428  stirlinglem5  27838  stirlinglem12  27845  lsatcmp  29266  lsatcmp2  29267  2atm  29789  trlatn0  30434  trlval3  30449  cdleme18c  30555  cdlemg17b  30924  cdlemg17i  30931  cdlemh  31079  dia2dimlem2  31328  dia2dimlem3  31329  dochlkr  31648  dochkrshp  31649  lcfl6  31763  lcfrlem9  31813  hdmap14lem6  32139  hgmapval0  32158
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