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

Theorem ord 370
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 363 . 2
31, 2sylib 190 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  \/wo 361
This theorem is referenced by:  orcanai  889  oplem1  940  ecase23d  1307  19.33b  1653  elpwunsn  3894  eqsn  4009  disji2  4254  disjxiun  4264  pwssun  4598  swopo  4622  somo  4646  ordtri3or  4722  ordtri1  4723  ordtri3  4726  ord0eln0  4744  suc11  4793  frsn  4880  foconst  5601  ordeleqon  6370  ssonprc  6373  onmindif2  6393  limsssuc  6431  limom  6461  onfununi  6761  oeeulem  7001  uniinqs  7141  pw2f1olem  7374  pssnn  7490  ordtypelem9  7687  ordtypelem10  7688  oismo  7701  preleq  7770  suc11reg  7772  cantnfp1lem2  7834  cantnflem1  7844  cantnfp1lem2OLD  7860  cantnflem1OLD  7867  cnfcom2lem  7881  cnfcom3lem  7883  cnfcom2lemOLD  7889  cnfcom3lemOLD  7891  rankxpsuc  8036  cardlim  8089  alephdom  8198  cardaleph  8206  iscard3  8210  pwcdadom  8332  cfslbn  8383  fin1a2lem12  8527  gchi  8737  fpwwe2lem13  8755  tskssel  8870  inttsk  8887  inar1  8888  r1tskina  8895  tskuni  8896  gruina  8931  grur1  8933  nlt1pi  9021  nqereu  9044  leltne  9410  nneo  10670  zeo2  10673  xrleltne  11067  nltpnft  11083  ngtmnft  11084  xrrebnd  11085  xaddf  11139  xrsupsslem  11214  xrinfmsslem  11215  seqf1olem1  11786  seqf1olem2  11787  discr1  11941  hashnncl  12075  seqcoll2  12158  sqeqd  12596  sqrmo  12682  isercoll  13086  dvdseq  13520  bitsfzo  13571  bitsinv1lem  13577  bitsf1  13582  bezoutlem3  13664  eucalglt  13700  phibndlem  13785  dfphi2  13789  prmdiv  13800  odzdvds  13807  pceq0  13877  pc2dvds  13885  fldivp1  13899  pcfac  13901  prmreclem3  13919  1arith  13928  4sqlem10  13948  4sqlem17  13962  4sqlem18  13963  vdwlem6  13987  ramubcl  14019  ramcl  14030  mrissmrcd  14518  psgnunilem5  15937  oddvdsnn0  15984  odnncl  15985  oddvds  15987  odcl2  16003  gexdvds  16020  gexnnod  16024  sylow1lem1  16034  odcau  16040  pgpssslw  16050  efgs1b  16170  efgredlema  16174  torsubg  16272  prmcyg  16306  gsumval3eu  16316  ablfacrplem  16432  ablfac1eu  16440  lspdisj  17015  lspsncv0  17036  fidomndrnglem  17186  gzrngunitlem  17587  prmirredlem  17625  prmirredlemOLD  17628  fctop  18312  cctop  18314  ppttop  18315  pptbas  18316  ordtrest2lem  18511  conclo  18723  txindis  18911  filcon  19160  ufilb  19183  cldsubg  19385  reconnlem1  20103  reconnlem2  20104  metds0  20126  metdseq0  20130  metnrmlem1a  20134  iccpnfhmeo  20217  xrhmeo  20218  cphsubrglem  20396  minveclem3b  20615  minveclem4a  20617  vitalilem4  20791  itg2gt0  20938  itgsplitioo  21015  limccnp2  21067  rollelem  21161  dvlip  21165  itgsubstlem  21220  plyaddlem1  21422  plymullem1  21423  coefv0  21456  dgreq0  21473  radcnv0  21622  pserdvlem2  21634  pilem2  21658  sineq0  21724  logtayl  21846  cxpsqr  21889  isosctrlem2  21958  atantayl2  22074  leibpilem1  22076  rlimcnp2  22101  amgm  22125  basellem3  22161  muval2  22213  sqf11  22218  ppinprm  22231  chtnprm  22233  perfectlem2  22310  lgsdir  22410  lgsabs1  22414  lgseisenlem1  22429  2sqlem7  22450  2sqblem  22457  chebbnd1lem1  22459  dchrisum0flblem1  22498  pntpbnd1  22576  pntpbnd2  22577  ostth  22629  minvecolem5  23961  staddi  25329  stadd3i  25331  atsseq  25430  atom1d  25436  atoml2i  25466  disji2f  25601  disjif2  25605  ordtrest2NEWlem  26061  eulerpartlemb  26454  subfacp1lem6  26776  cvmscld  26865  cvmsss2  26866  cvmseu  26868  ordtoplem  27984  ordcmp  27996  heiborlem6  28386  isfldidl  28539  pridlc2  28543  ctbnfien  28830  pw2f1ocnv  29059  unxpwdom3  29121  dgrsub2  29164  fmul01lt1lem1  29438  stoweidlem35  29504  stirlinglem5  29547  stirlinglem12  29554  lsatcmp  32085  lsatcmp2  32086  2atm  32608  trlatn0  33253  trlval3  33268  cdleme18c  33374  cdlemg17b  33743  cdlemg17i  33750  cdlemh  33898  dia2dimlem2  34147  dia2dimlem3  34148  dochlkr  34467  dochkrshp  34468  lcfl6  34582  lcfrlem9  34632  hdmap14lem6  34958  hgmapval0  34977
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 179  df-or 363
  Copyright terms: Public domain W3C validator