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

Theorem ord 390
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 383 . 2 ((𝜓𝜒) ↔ (¬ 𝜓𝜒))
31, 2sylib 206 1 (𝜑 → (¬ 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 381
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 195  df-or 383
This theorem is referenced by:  ornld  937  orcanai  949  oplem1  998  ecase23d  1427  19.33b  1800  elpwunsn  4166  eqsnOLD  4295  disji2  4559  disjxiun  4569  disjxiunOLD  4570  pwssun  4930  swopo  4955  sotric  4971  sotrieq  4972  somo  4979  ordtri3or  5654  ordtri1  5655  ordtri3OLD  5659  suc11  5730  foconst  6020  ordeleqon  6853  ssonprc  6857  onmindif2  6877  limsssuc  6915  limom  6945  onfununi  7298  oeeulem  7541  uniinqs  7687  pw2f1olem  7922  pssnn  8036  ordtypelem9  8287  ordtypelem10  8288  oismo  8301  preleq  8370  suc11reg  8372  cantnfp1lem2  8432  cantnflem1  8442  cnfcom2lem  8454  cnfcom3lem  8456  rankxpsuc  8601  cardlim  8654  alephdom  8760  cardaleph  8768  iscard3  8772  pwcdadom  8894  cfslbn  8945  fin1a2lem12  9089  gchi  9298  fpwwe2lem13  9316  tskssel  9431  inttsk  9448  inar1  9449  r1tskina  9456  tskuni  9457  gruina  9492  grur1  9494  nlt1pi  9580  nqereu  9603  leltne  9974  nneo  11289  zeo2  11292  xrleltne  11809  nltpnft  11826  ngtmnft  11827  xrrebnd  11828  xaddf  11884  xrsupsslem  11961  xrinfmsslem  11962  fzocatel  12350  seqf1olem1  12653  seqf1olem2  12654  discr1  12813  hashnncl  12966  seqcoll2  13054  sqeqd  13696  sqrmo  13782  isercoll  14188  bitsfzo  14937  bitsinv1lem  14943  bitsf1  14948  bezoutlem3  15038  eucalglt  15078  phibndlem  15255  dfphi2  15259  prmdiv  15270  odzdvds  15280  pceq0  15355  pc2dvds  15363  fldivp1  15381  pcfac  15383  prmreclem3  15402  1arith  15411  4sqlem10  15431  4sqlem17  15445  4sqlem18  15446  vdwlem6  15470  ramubcl  15502  ramcl  15513  mrissmrcd  16065  psgnunilem5  17679  oddvdsnn0  17728  odnncl  17729  oddvds  17731  odcl2  17747  gexdvds  17764  gexnnod  17768  sylow1lem1  17778  odcau  17784  pgpssslw  17794  efgs1b  17914  efgredlema  17918  torsubg  18022  prmcyg  18060  gsumval3eu  18070  ablfacrplem  18229  ablfac1eu  18237  lspdisj  18888  lspsncv0  18909  fidomndrnglem  19069  gzrngunitlem  19572  prmirredlem  19601  fctop  20556  cctop  20558  ppttop  20559  pptbas  20560  ordtrest2lem  20755  conclo  20966  txindis  21185  filcon  21435  ufilb  21458  cldsubg  21662  reconnlem1  22365  reconnlem2  22366  metds0  22388  metdseq0  22392  metnrmlem1a  22396  iccpnfhmeo  22479  xrhmeo  22480  cphsubrglem  22705  minveclem3b  22920  minveclem4a  22922  vitalilem4  23099  itg2gt0  23246  itgsplitioo  23323  limccnp2  23375  rollelem  23469  dvlip  23473  itgsubstlem  23528  plyaddlem1  23686  plymullem1  23687  coefv0  23721  dgreq0  23738  radcnv0  23887  pserdvlem2  23899  pilem2  23923  sineq0  23990  logtayl  24119  cxpsqrt  24162  isosctrlem2  24262  atantayl2  24378  leibpilem1  24380  rlimcnp2  24406  amgm  24430  basellem3  24522  muval2  24573  sqf11  24578  ppinprm  24591  chtnprm  24593  perfectlem2  24668  lgsdir  24770  lgsabs1  24774  lgseisenlem1  24813  2sqlem7  24862  2sqblem  24869  chebbnd1lem1  24871  dchrisum0flblem1  24910  pntpbnd1  24988  pntpbnd2  24989  ostth  25041  symquadlem  25298  midexlem  25301  colperp  25335  midex  25343  oppperpex  25359  outpasch  25361  hlpasch  25362  hpgerlem  25371  colopp  25375  colhp  25376  lmieu  25390  lmicom  25394  trgcopy  25410  cgracol  25433  minvecolem5  26923  staddi  28291  stadd3i  28293  atsseq  28392  atom1d  28398  atoml2i  28428  disji2f  28574  disjif2  28578  znsqcld  28702  2sqmod  28781  psgnfzto1stlem  28983  ordtrest2NEWlem  29098  eulerpartlemb  29559  sgn3da  29732  subfacp1lem6  30223  cvmscld  30311  cvmsss2  30312  cvmseu  30314  nosepon  30868  ordtoplem  31406  ordcmp  31418  poimirlem25  32403  heiborlem6  32584  isfldidl  32836  pridlc2  32840  mpt2bi123f  32940  mptbi12f  32944  ac6s6  32949  lsatcmp  33107  lsatcmp2  33108  2atm  33630  trlatn0  34276  trlval3  34291  cdleme18c  34397  cdlemg17b  34767  cdlemg17i  34774  cdlemh  34922  dia2dimlem2  35171  dia2dimlem3  35172  dochlkr  35491  dochkrshp  35492  lcfl6  35606  lcfrlem9  35656  hdmap14lem6  35982  hgmapval0  36001  ctbnfien  36199  pw2f1ocnv  36421  unxpwdom3  36482  dgrsub2  36523  rp-fakeanorass  36676  disjxp1  38062  fmul01lt1lem1  38451  elprn1  38500  stoweidlem35  38728  stirlinglem5  38771  stirlinglem12  38778  fourierdlem42  38842  fourierdlem93  38892  perfectALTVlem2  39966
  Copyright terms: Public domain W3C validator