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

Theorem ord 882
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 866 . 2 ((𝜓𝜒) ↔ (¬ 𝜓𝜒))
31, 2sylib 209 1 (𝜑 → (¬ 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 865
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 198  df-or 866
This theorem is referenced by:  orcanai  1016  oplem1  1072  ornld  1077  ecase23d  1590  19.33b  1975  elpwunsn  4411  disji2  4821  disjxiun  4834  pwssun  5209  swopo  5236  sotric  5252  sotrieq  5253  somo  5260  ordtri3or  5962  ordtri1  5963  ordtri3OLD  5967  suc11  6038  foconst  6336  ordeleqon  7212  ssonprc  7216  onmindif2  7236  limsssuc  7274  limom  7304  onfununi  7668  oeeulem  7912  uniinqs  8056  pw2f1olem  8297  pssnn  8411  ordtypelem9  8664  ordtypelem10  8665  oismo  8678  preleqALT  8753  preleqOLD  8755  suc11reg  8757  cantnfp1lem2  8817  cantnflem1  8827  cnfcom2lem  8839  cnfcom3lem  8841  rankxpsuc  8986  cardlim  9075  alephdom  9181  cardaleph  9189  iscard3  9193  pwcdadom  9317  cfslbn  9368  fin1a2lem12  9512  gchi  9725  fpwwe2lem13  9743  tskssel  9858  inttsk  9875  inar1  9876  r1tskina  9883  tskuni  9884  gruina  9919  grur1  9921  nlt1pi  10007  nqereu  10030  leltne  10406  nneo  11721  zeo2  11724  xrleltne  12188  nltpnft  12207  ngtmnft  12209  xrrebnd  12211  xaddf  12267  xrsupsslem  12349  xrinfmsslem  12350  fzocatel  12750  seqf1olem1  13057  seqf1olem2  13058  discr1  13217  hashnncl  13369  seqcoll2  13460  sqeqd  14123  sqrmo  14209  isercoll  14615  bitsfzo  15370  bitsinv1lem  15376  bitsf1  15381  bezoutlem3  15471  eucalglt  15511  phibndlem  15686  dfphi2  15690  prmdiv  15701  odzdvds  15711  pceq0  15786  pc2dvds  15794  fldivp1  15812  pcfac  15814  prmreclem3  15833  1arith  15842  4sqlem10  15862  4sqlem17  15876  4sqlem18  15877  vdwlem6  15901  ramubcl  15933  ramcl  15944  mrissmrcd  16499  psgnunilem5  18109  oddvdsnn0  18158  odnncl  18159  oddvds  18161  odcl2  18177  gexdvds  18194  gexnnod  18198  sylow1lem1  18208  odcau  18214  pgpssslw  18224  efgs1b  18344  efgredlema  18348  torsubg  18452  prmcyg  18490  gsumval3eu  18500  ablfacrplem  18660  ablfac1eu  18668  lspdisj  19326  lspsncv0  19348  lspsncv0OLD  19349  fidomndrnglem  19509  gzrngunitlem  20013  prmirredlem  20043  fctop  21016  cctop  21018  ppttop  21019  pptbas  21020  ordtrest2lem  21215  connclo  21426  txindis  21645  filconn  21894  ufilb  21917  cldsubg  22121  reconnlem1  22836  reconnlem2  22837  metds0  22860  metdseq0  22864  metnrmlem1a  22868  iccpnfhmeo  22951  xrhmeo  22952  cphsubrglem  23183  minveclem3b  23405  minveclem4a  23407  vitalilem4  23586  itg2gt0  23735  itgsplitioo  23812  limccnp2  23864  rollelem  23960  dvlip  23964  itgsubstlem  24019  plyaddlem1  24177  plymullem1  24178  coefv0  24212  dgreq0  24229  radcnv0  24378  pserdvlem2  24390  pilem2  24414  sineq0  24482  logtayl  24614  cxpsqrt  24657  isosctrlem2  24757  atantayl2  24873  leibpilem1  24875  rlimcnp2  24901  amgm  24925  basellem3  25017  muval2  25068  sqf11  25073  ppinprm  25086  chtnprm  25088  perfectlem2  25163  lgsdir  25265  lgsabs1  25269  lgseisenlem1  25308  2sqlem7  25357  2sqblem  25364  chebbnd1lem1  25366  dchrisum0flblem1  25405  pntpbnd1  25483  pntpbnd2  25484  ostth  25536  symquadlem  25792  midexlem  25795  colperp  25829  midex  25837  oppperpex  25853  outpasch  25855  hlpasch  25856  hpgerlem  25865  colopp  25869  colhp  25870  lmieu  25884  lmicom  25888  trgcopy  25904  cgracol  25927  minvecolem5  28059  staddi  29427  stadd3i  29429  atsseq  29528  atom1d  29534  atoml2i  29564  disji2f  29709  disjif2  29713  znsqcld  29833  fprodex01  29892  2sqmod  29967  psgnfzto1stlem  30169  ordtrest2NEWlem  30287  eulerpartlemb  30749  sgn3da  30922  subfacp1lem6  31484  cvmscld  31572  cvmsss2  31573  cvmseu  31575  nosepon  32133  ordtoplem  32745  ordcmp  32757  poimirlem25  33741  heiborlem6  33920  isfldidl  34172  pridlc2  34176  mpt2bi123f  34275  mptbi12f  34279  ac6s6  34284  lsatcmp  34777  lsatcmp2  34778  2atm  35301  trlatn0  35947  trlval3  35962  cdleme18c  36068  cdlemg17b  36437  cdlemg17i  36444  cdlemh  36592  dia2dimlem2  36840  dia2dimlem3  36841  dochlkr  37160  dochkrshp  37161  lcfl6  37275  lcfrlem9  37325  hdmap14lem6  37648  hgmapval0  37667  ioin9i8  37742  ctbnfien  37878  pw2f1ocnv  38099  unxpwdom3  38160  dgrsub2  38200  rp-fakeanorass  38352  disjxp1  39725  fmul01lt1lem1  40290  elprn1  40339  stoweidlem35  40725  stirlinglem5  40768  stirlinglem12  40775  fourierdlem42  40839  fourierdlem93  40889  perfectALTVlem2  42200
  Copyright terms: Public domain W3C validator