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

Theorem ord 391
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 384 . 2 ((𝜓𝜒) ↔ (¬ 𝜓𝜒))
31, 2sylib 208 1 (𝜑 → (¬ 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 382
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 197  df-or 384
This theorem is referenced by:  ornld  958  orcanai  972  oplem1  1027  ecase23d  1476  19.33b  1853  elpwunsn  4256  eqsnOLD  4394  disji2  4668  disjxiun  4681  disjxiunOLD  4682  pwssun  5049  swopo  5074  sotric  5090  sotrieq  5091  somo  5098  ordtri3or  5793  ordtri1  5794  ordtri3OLD  5798  suc11  5869  foconst  6164  ordeleqon  7030  ssonprc  7034  onmindif2  7054  limsssuc  7092  limom  7122  onfununi  7483  oeeulem  7726  uniinqs  7870  pw2f1olem  8105  pssnn  8219  ordtypelem9  8472  ordtypelem10  8473  oismo  8486  preleq  8552  suc11reg  8554  cantnfp1lem2  8614  cantnflem1  8624  cnfcom2lem  8636  cnfcom3lem  8638  rankxpsuc  8783  cardlim  8836  alephdom  8942  cardaleph  8950  iscard3  8954  pwcdadom  9076  cfslbn  9127  fin1a2lem12  9271  gchi  9484  fpwwe2lem13  9502  tskssel  9617  inttsk  9634  inar1  9635  r1tskina  9642  tskuni  9643  gruina  9678  grur1  9680  nlt1pi  9766  nqereu  9789  leltne  10165  nneo  11499  zeo2  11502  xrleltne  12016  nltpnft  12033  ngtmnft  12035  xrrebnd  12037  xaddf  12093  xrsupsslem  12175  xrinfmsslem  12176  fzocatel  12571  seqf1olem1  12880  seqf1olem2  12881  discr1  13040  hashnncl  13195  seqcoll2  13287  sqeqd  13950  sqrmo  14036  isercoll  14442  bitsfzo  15204  bitsinv1lem  15210  bitsf1  15215  bezoutlem3  15305  eucalglt  15345  phibndlem  15522  dfphi2  15526  prmdiv  15537  odzdvds  15547  pceq0  15622  pc2dvds  15630  fldivp1  15648  pcfac  15650  prmreclem3  15669  1arith  15678  4sqlem10  15698  4sqlem17  15712  4sqlem18  15713  vdwlem6  15737  ramubcl  15769  ramcl  15780  mrissmrcd  16347  psgnunilem5  17960  oddvdsnn0  18009  odnncl  18010  oddvds  18012  odcl2  18028  gexdvds  18045  gexnnod  18049  sylow1lem1  18059  odcau  18065  pgpssslw  18075  efgs1b  18195  efgredlema  18199  torsubg  18303  prmcyg  18341  gsumval3eu  18351  ablfacrplem  18510  ablfac1eu  18518  lspdisj  19173  lspsncv0  19194  fidomndrnglem  19354  gzrngunitlem  19859  prmirredlem  19889  fctop  20856  cctop  20858  ppttop  20859  pptbas  20860  ordtrest2lem  21055  connclo  21266  txindis  21485  filconn  21734  ufilb  21757  cldsubg  21961  reconnlem1  22676  reconnlem2  22677  metds0  22700  metdseq0  22704  metnrmlem1a  22708  iccpnfhmeo  22791  xrhmeo  22792  cphsubrglem  23023  minveclem3b  23245  minveclem4a  23247  vitalilem4  23425  itg2gt0  23572  itgsplitioo  23649  limccnp2  23701  rollelem  23797  dvlip  23801  itgsubstlem  23856  plyaddlem1  24014  plymullem1  24015  coefv0  24049  dgreq0  24066  radcnv0  24215  pserdvlem2  24227  pilem2  24251  sineq0  24318  logtayl  24451  cxpsqrt  24494  isosctrlem2  24594  atantayl2  24710  leibpilem1  24712  rlimcnp2  24738  amgm  24762  basellem3  24854  muval2  24905  sqf11  24910  ppinprm  24923  chtnprm  24925  perfectlem2  25000  lgsdir  25102  lgsabs1  25106  lgseisenlem1  25145  2sqlem7  25194  2sqblem  25201  chebbnd1lem1  25203  dchrisum0flblem1  25242  pntpbnd1  25320  pntpbnd2  25321  ostth  25373  symquadlem  25629  midexlem  25632  colperp  25666  midex  25674  oppperpex  25690  outpasch  25692  hlpasch  25693  hpgerlem  25702  colopp  25706  colhp  25707  lmieu  25721  lmicom  25725  trgcopy  25741  cgracol  25764  minvecolem5  27865  staddi  29233  stadd3i  29235  atsseq  29334  atom1d  29340  atoml2i  29370  disji2f  29516  disjif2  29520  znsqcld  29640  fprodex01  29699  2sqmod  29776  psgnfzto1stlem  29978  ordtrest2NEWlem  30096  eulerpartlemb  30558  sgn3da  30731  subfacp1lem6  31293  cvmscld  31381  cvmsss2  31382  cvmseu  31384  nosepon  31943  ordtoplem  32559  ordcmp  32571  poimirlem25  33564  heiborlem6  33745  isfldidl  33997  pridlc2  34001  mpt2bi123f  34101  mptbi12f  34105  ac6s6  34110  lsatcmp  34608  lsatcmp2  34609  2atm  35131  trlatn0  35777  trlval3  35792  cdleme18c  35898  cdlemg17b  36267  cdlemg17i  36274  cdlemh  36422  dia2dimlem2  36671  dia2dimlem3  36672  dochlkr  36991  dochkrshp  36992  lcfl6  37106  lcfrlem9  37156  hdmap14lem6  37482  hgmapval0  37501  ctbnfien  37699  pw2f1ocnv  37921  unxpwdom3  37982  dgrsub2  38022  rp-fakeanorass  38175  disjxp1  39552  fmul01lt1lem1  40134  elprn1  40183  stoweidlem35  40570  stirlinglem5  40613  stirlinglem12  40620  fourierdlem42  40684  fourierdlem93  40734  perfectALTVlem2  41956
  Copyright terms: Public domain W3C validator