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

Theorem ord 863
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 847 . 2 ((𝜓𝜒) ↔ (¬ 𝜓𝜒))
31, 2sylib 217 1 (𝜑 → (¬ 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 846
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 206  df-or 847
This theorem is referenced by:  olcnd  876  orcanai  1002  ecase2d  1029  oplem1  1056  ornld  1061  ecase23d  1474  19.33b  1889  elpwunsn  4649  disji2  5092  disjxiun  5107  pwssun  5533  swopo  5561  sotric  5578  sotrieq  5579  somo  5587  ordtri3or  6354  ordtri1  6355  suc11  6429  foconst  6776  ordeleqon  7721  ssonprc  7727  onmindif2  7747  limsssuc  7791  limom  7823  onfununi  8292  oeeulem  8553  uniinqs  8743  pw2f1olem  9027  pssnn  9119  pssnnOLD  9216  ordtypelem9  9469  ordtypelem10  9470  oismo  9483  preleqALT  9560  suc11reg  9562  cantnfp1lem2  9622  cantnflem1  9632  cnfcom2lem  9644  cnfcom3lem  9646  rankxpsuc  9825  cardlim  9915  alephdom  10024  cardaleph  10032  iscard3  10036  pwdjudom  10159  cfslbn  10210  fin1a2lem12  10354  gchi  10567  tskssel  10700  inttsk  10717  inar1  10718  r1tskina  10725  tskuni  10726  gruina  10761  grur1  10763  nlt1pi  10849  nqereu  10872  leltne  11251  nneo  12594  zeo2  12597  xrleltne  13071  nltpnft  13090  ngtmnft  13092  xrrebnd  13094  xaddf  13150  xrsupsslem  13233  xrinfmsslem  13234  fzocatel  13643  seqf1olem1  13954  seqf1olem2  13955  znsqcld  14074  discr1  14149  hashnncl  14273  seqcoll2  14371  sqeqd  15058  sqrmo  15143  isercoll  15559  bitsfzo  16322  bitsinv1lem  16328  bitsf1  16333  bezoutlem3  16429  eucalglt  16468  phibndlem  16649  dfphi2  16653  prmdiv  16664  odzdvds  16674  pceq0  16750  pc2dvds  16758  fldivp1  16776  pcfac  16778  prmreclem3  16797  1arith  16806  4sqlem10  16826  4sqlem17  16840  4sqlem18  16841  vdwlem6  16865  ramubcl  16897  ramcl  16908  mrissmrcd  17527  psgnunilem5  19283  oddvdsnn0  19333  odnncl  19334  oddvds  19336  odcl2  19354  gexdvds  19373  gexnnod  19377  sylow1lem1  19387  odcau  19393  pgpssslw  19403  efgs1b  19525  efgredlema  19529  torsubg  19639  prmcyg  19678  gsumval3eu  19688  ablfacrplem  19851  ablfac1eu  19859  ablsimpgprmd  19901  lspdisj  20602  lspsncv0  20623  fidomndrnglem  20793  gzrngunitlem  20878  prmirredlem  20909  fctop  22370  cctop  22372  ppttop  22373  pptbas  22374  ordtrest2lem  22570  connclo  22782  txindis  23001  filconn  23250  ufilb  23273  cldsubg  23478  reconnlem1  24205  reconnlem2  24206  metds0  24229  metdseq0  24233  metnrmlem1a  24237  iccpnfhmeo  24324  xrhmeo  24325  cphsubrglem  24557  minveclem3b  24808  minveclem4a  24810  vitalilem4  24991  itg2gt0  25141  itgsplitioo  25218  limccnp2  25272  rollelem  25369  dvlip  25373  itgsubstlem  25428  plyaddlem1  25590  plymullem1  25591  coefv0  25625  dgreq0  25642  radcnv0  25791  pserdvlem2  25803  pilem2  25827  sineq0  25896  logtayl  26031  cxpsqrt  26074  isosctrlem2  26185  atantayl2  26304  rlimcnp2  26332  amgm  26356  basellem3  26448  muval2  26499  sqf11  26504  ppinprm  26517  chtnprm  26519  perfectlem2  26594  lgsdir  26696  lgsabs1  26700  lgseisenlem1  26739  2sqlem7  26788  2sqblem  26795  2sqmod  26800  2sqreultblem  26812  2sqreunnltblem  26815  chebbnd1lem1  26833  dchrisum0flblem1  26872  pntpbnd1  26950  pntpbnd2  26951  ostth  27003  nosepon  27029  symquadlem  27673  midexlem  27676  colperp  27713  midex  27721  oppperpex  27737  hlpasch  27740  hpgerlem  27749  colopp  27753  lmieu  27768  lmicom  27772  trgcopy  27788  cgracol  27812  minvecolem5  29865  staddi  31230  stadd3i  31232  atsseq  31331  atom1d  31337  atoml2i  31367  disji2f  31537  disjif2  31541  fprodex01  31763  psgnfzto1stlem  31991  lvecdim0  32344  ordtrest2NEWlem  32543  eulerpartlemb  33008  sgn3da  33181  subfacp1lem6  33819  cvmscld  33907  cvmsss2  33908  cvmseu  33910  ordtoplem  34936  ordcmp  34948  poimirlem25  36132  heiborlem6  36304  isfldidl  36556  pridlc2  36560  mpobi123f  36650  mptbi12f  36654  ac6s6  36660  lsatcmp  37494  lsatcmp2  37495  2atm  38019  trlatn0  38664  trlval3  38679  cdleme18c  38785  cdlemg17b  39154  cdlemg17i  39161  cdlemh  39309  dia2dimlem2  39557  dia2dimlem3  39558  dochlkr  39877  dochkrshp  39878  lcfl6  39992  lcfrlem9  40042  hdmap14lem6  40365  hgmapval0  40384  ioin9i8  40654  ctbnfien  41170  pw2f1ocnv  41390  unxpwdom3  41451  dgrsub2  41491  dflim5  41693  rp-fakeanorass  41859  mnuprdlem1  42626  mnuprdlem2  42627  mnurndlem1  42635  disjxp1  43351  fmul01lt1lem1  43899  elprn1  43948  stoweidlem35  44350  stirlinglem5  44393  stirlinglem12  44400  fourierdlem42  44464  fourierdlem93  44514  perfectALTVlem2  45988
  Copyright terms: Public domain W3C validator