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:  ornld  898  orcanai  913  oplem1  964  ecase23d  1332  19.33b  1696  elpwunsn  4070  eqsn  4191  disji2  4439  disjxiun  4449  pwssun  4791  swopo  4815  somo  4839  ordtri3or  4915  ordtri1  4916  ordtri3  4919  ord0eln0  4937  suc11  4986  frsn  5075  foconst  5811  ordeleqon  6624  ssonprc  6627  onmindif2  6647  limsssuc  6685  limom  6715  onfununi  7031  oeeulem  7269  uniinqs  7410  pw2f1olem  7641  pssnn  7758  ordtypelem9  7972  ordtypelem10  7973  oismo  7986  preleq  8055  suc11reg  8057  cantnfp1lem2  8119  cantnflem1  8129  cantnfp1lem2OLD  8145  cantnflem1OLD  8152  cnfcom2lem  8166  cnfcom3lem  8168  cnfcom2lemOLD  8174  cnfcom3lemOLD  8176  rankxpsuc  8321  cardlim  8374  alephdom  8483  cardaleph  8491  iscard3  8495  pwcdadom  8617  cfslbn  8668  fin1a2lem12  8812  gchi  9023  fpwwe2lem13  9041  tskssel  9156  inttsk  9173  inar1  9174  r1tskina  9181  tskuni  9182  gruina  9217  grur1  9219  nlt1pi  9305  nqereu  9328  leltne  9695  nneo  10971  zeo2  10974  xrleltne  11380  nltpnft  11396  ngtmnft  11397  xrrebnd  11398  xaddf  11452  xrsupsslem  11527  xrinfmsslem  11528  fzocatel  11880  seqf1olem1  12146  seqf1olem2  12147  discr1  12302  hashnncl  12436  seqcoll2  12513  sqeqd  12999  sqrmo  13085  isercoll  13490  dvdseq  14033  bitsfzo  14085  bitsinv1lem  14091  bitsf1  14096  bezoutlem3  14178  eucalglt  14214  phibndlem  14300  dfphi2  14304  prmdiv  14315  odzdvds  14322  pceq0  14394  pc2dvds  14402  fldivp1  14416  pcfac  14418  prmreclem3  14436  1arith  14445  4sqlem10  14465  4sqlem17  14479  4sqlem18  14480  vdwlem6  14504  ramubcl  14536  ramcl  14547  mrissmrcd  15037  psgnunilem5  16519  oddvdsnn0  16568  odnncl  16569  oddvds  16571  odcl2  16587  gexdvds  16604  gexnnod  16608  sylow1lem1  16618  odcau  16624  pgpssslw  16634  efgs1b  16754  efgredlema  16758  torsubg  16860  prmcyg  16896  gsumval3eu  16907  ablfacrplem  17116  ablfac1eu  17124  lspdisj  17771  lspsncv0  17792  fidomndrnglem  17955  gzrngunitlem  18482  prmirredlem  18523  prmirredlemOLD  18526  fctop  19505  cctop  19507  ppttop  19508  pptbas  19509  ordtrest2lem  19704  conclo  19916  txindis  20135  filcon  20384  ufilb  20407  cldsubg  20609  reconnlem1  21331  reconnlem2  21332  metds0  21354  metdseq0  21358  metnrmlem1a  21362  iccpnfhmeo  21445  xrhmeo  21446  cphsubrglem  21624  minveclem3b  21843  minveclem4a  21845  vitalilem4  22020  itg2gt0  22167  itgsplitioo  22244  limccnp2  22296  rollelem  22390  dvlip  22394  itgsubstlem  22449  plyaddlem1  22610  plymullem1  22611  coefv0  22645  dgreq0  22662  radcnv0  22811  pserdvlem2  22823  pilem2  22847  sineq0  22914  logtayl  23041  cxpsqrt  23084  isosctrlem2  23153  atantayl2  23269  leibpilem1  23271  rlimcnp2  23296  amgm  23320  basellem3  23356  muval2  23408  sqf11  23413  ppinprm  23426  chtnprm  23428  perfectlem2  23505  lgsdir  23605  lgsabs1  23609  lgseisenlem1  23624  2sqlem7  23645  2sqblem  23652  chebbnd1lem1  23654  dchrisum0flblem1  23693  pntpbnd1  23771  pntpbnd2  23772  ostth  23824  coltr2  24028  symquadlem  24066  midexlem  24069  colperp  24103  midex  24111  hpgerlem  24134  lmieu  24150  lmicom  24154  minvecolem5  25797  staddi  27165  stadd3i  27167  atsseq  27266  atom1d  27272  atoml2i  27302  disji2f  27438  disjif2  27442  znsqcld  27561  2sqmod  27636  ordtrest2NEWlem  27904  eulerpartlemb  28307  sgn3da  28480  subfacp1lem6  28629  cvmscld  28718  cvmsss2  28719  cvmseu  28721  ordtoplem  29900  ordcmp  29912  heiborlem6  30312  isfldidl  30465  pridlc2  30469  mpt2bi123f  30571  mptbi12f  30575  ac6s6  30580  ctbnfien  30752  pw2f1ocnv  30979  unxpwdom3  31041  dgrsub2  31084  fmul01lt1lem1  31578  elprn1  31639  stoweidlem35  31817  stirlinglem5  31860  stirlinglem12  31867  fourierdlem42  31931  fourierdlem93  31982  lsatcmp  34728  lsatcmp2  34729  2atm  35251  trlatn0  35897  trlval3  35912  cdleme18c  36018  cdlemg17b  36388  cdlemg17i  36395  cdlemh  36543  dia2dimlem2  36792  dia2dimlem3  36793  dochlkr  37112  dochkrshp  37113  lcfl6  37227  lcfrlem9  37277  hdmap14lem6  37603  hgmapval0  37622  rp-fakeanorass  37737
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