MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ord Unicode version

Theorem ord 377
Description: Deduce implication from disjunction. (Contributed by NM, 18-May-1994.)
Hypothesis
Ref Expression
ord.1
Assertion
Ref Expression
ord

Proof of Theorem ord
StepHypRef Expression
1 ord.1 . 2
2 df-or 370 . 2
31, 2sylib 196 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  \/wo 368
This theorem is referenced by:  orcanai  904  oplem1  955  ecase23d  1323  19.33b  1664  elpwunsn  4034  eqsn  4151  disji2  4396  disjxiun  4406  pwssun  4744  swopo  4768  somo  4792  ordtri3or  4868  ordtri1  4869  ordtri3  4872  ord0eln0  4890  suc11  4939  frsn  5026  foconst  5753  ordeleqon  6533  ssonprc  6536  onmindif2  6556  limsssuc  6594  limom  6624  onfununi  6936  oeeulem  7174  uniinqs  7314  pw2f1olem  7549  pssnn  7666  ordtypelem9  7877  ordtypelem10  7878  oismo  7891  preleq  7960  suc11reg  7962  cantnfp1lem2  8024  cantnflem1  8034  cantnfp1lem2OLD  8050  cantnflem1OLD  8057  cnfcom2lem  8071  cnfcom3lem  8073  cnfcom2lemOLD  8079  cnfcom3lemOLD  8081  rankxpsuc  8226  cardlim  8279  alephdom  8388  cardaleph  8396  iscard3  8400  pwcdadom  8522  cfslbn  8573  fin1a2lem12  8717  gchi  8928  fpwwe2lem13  8946  tskssel  9061  inttsk  9078  inar1  9079  r1tskina  9086  tskuni  9087  gruina  9122  grur1  9124  nlt1pi  9212  nqereu  9235  leltne  9601  nneo  10863  zeo2  10866  xrleltne  11261  nltpnft  11277  ngtmnft  11278  xrrebnd  11279  xaddf  11333  xrsupsslem  11408  xrinfmsslem  11409  seqf1olem1  12002  seqf1olem2  12003  discr1  12157  hashnncl  12291  seqcoll2  12375  sqeqd  12813  sqrmo  12899  isercoll  13303  dvdseq  13738  bitsfzo  13789  bitsinv1lem  13795  bitsf1  13800  bezoutlem3  13882  eucalglt  13918  phibndlem  14003  dfphi2  14007  prmdiv  14018  odzdvds  14025  pceq0  14095  pc2dvds  14103  fldivp1  14117  pcfac  14119  prmreclem3  14137  1arith  14146  4sqlem10  14166  4sqlem17  14180  4sqlem18  14181  vdwlem6  14205  ramubcl  14237  ramcl  14248  mrissmrcd  14737  psgnunilem5  16159  oddvdsnn0  16208  odnncl  16209  oddvds  16211  odcl2  16227  gexdvds  16244  gexnnod  16248  sylow1lem1  16258  odcau  16264  pgpssslw  16274  efgs1b  16394  efgredlema  16398  torsubg  16497  prmcyg  16531  gsumval3eu  16542  ablfacrplem  16741  ablfac1eu  16749  lspdisj  17382  lspsncv0  17403  fidomndrnglem  17554  gzrngunitlem  18070  prmirredlem  18110  prmirredlemOLD  18113  fctop  19007  cctop  19009  ppttop  19010  pptbas  19011  ordtrest2lem  19206  conclo  19418  txindis  19606  filcon  19855  ufilb  19878  cldsubg  20080  reconnlem1  20802  reconnlem2  20803  metds0  20825  metdseq0  20829  metnrmlem1a  20833  iccpnfhmeo  20916  xrhmeo  20917  cphsubrglem  21095  minveclem3b  21314  minveclem4a  21316  vitalilem4  21491  itg2gt0  21638  itgsplitioo  21715  limccnp2  21767  rollelem  21861  dvlip  21865  itgsubstlem  21920  plyaddlem1  22081  plymullem1  22082  coefv0  22115  dgreq0  22132  radcnv0  22281  pserdvlem2  22293  pilem2  22317  sineq0  22383  logtayl  22505  cxpsqr  22548  isosctrlem2  22617  atantayl2  22733  leibpilem1  22735  rlimcnp2  22760  amgm  22784  basellem3  22820  muval2  22872  sqf11  22877  ppinprm  22890  chtnprm  22892  perfectlem2  22969  lgsdir  23069  lgsabs1  23073  lgseisenlem1  23088  2sqlem7  23109  2sqblem  23116  chebbnd1lem1  23118  dchrisum0flblem1  23157  pntpbnd1  23235  pntpbnd2  23236  ostth  23288  coltr2  23477  colmid  23509  symquadlem  23510  midexlem  23513  colperp  23544  mideu  23550  lmieu  23563  lmicom  23567  lmiisolem  23574  minvecolem5  24751  staddi  26119  stadd3i  26121  atsseq  26220  atom1d  26226  atoml2i  26256  disji2f  26389  disjif2  26393  ordtrest2NEWlem  26809  eulerpartlemb  27207  subfacp1lem6  27529  cvmscld  27618  cvmsss2  27619  cvmseu  27621  ordtoplem  28737  ordcmp  28749  heiborlem6  29175  isfldidl  29328  pridlc2  29332  mpt2bi123f  29435  mptbi12f  29439  ac6s6  29444  ctbnfien  29617  pw2f1ocnv  29846  unxpwdom3  29908  dgrsub2  29951  fmul01lt1lem1  30363  stoweidlem35  30564  stirlinglem5  30607  stirlinglem12  30614  fourierdlem42  30678  lsatcmp  33499  lsatcmp2  33500  2atm  34022  trlatn0  34667  trlval3  34682  cdleme18c  34788  cdlemg17b  35157  cdlemg17i  35164  cdlemh  35312  dia2dimlem2  35561  dia2dimlem3  35562  dochlkr  35881  dochkrshp  35882  lcfl6  35996  lcfrlem9  36046  hdmap14lem6  36372  hgmapval0  36391
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-or 370
  Copyright terms: Public domain W3C validator