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

Theorem ord 861
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 845 . 2 ((𝜓𝜒) ↔ (¬ 𝜓𝜒))
31, 2sylib 221 1 (𝜑 → (¬ 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 844
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 210  df-or 845
This theorem is referenced by:  olcnd  874  orcanai  1000  oplem1  1052  ornld  1057  ecase23d  1470  19.33b  1886  elpwunsn  4581  disji2  5012  disjxiun  5027  pwssun  5421  swopo  5448  sotric  5465  sotrieq  5466  somo  5474  ordtri3or  6191  ordtri1  6192  suc11  6262  foconst  6578  ordeleqon  7483  ssonprc  7487  onmindif2  7507  limsssuc  7545  limom  7575  onfununi  7961  oeeulem  8210  uniinqs  8360  pw2f1olem  8604  pssnn  8720  ordtypelem9  8974  ordtypelem10  8975  oismo  8988  preleqALT  9064  suc11reg  9066  cantnfp1lem2  9126  cantnflem1  9136  cnfcom2lem  9148  cnfcom3lem  9150  rankxpsuc  9295  cardlim  9385  alephdom  9492  cardaleph  9500  iscard3  9504  pwdjudom  9627  cfslbn  9678  fin1a2lem12  9822  gchi  10035  fpwwe2lem13  10053  tskssel  10168  inttsk  10185  inar1  10186  r1tskina  10193  tskuni  10194  gruina  10229  grur1  10231  nlt1pi  10317  nqereu  10340  leltne  10719  nneo  12054  zeo2  12057  xrleltne  12526  nltpnft  12545  ngtmnft  12547  xrrebnd  12549  xaddf  12605  xrsupsslem  12688  xrinfmsslem  12689  fzocatel  13096  seqf1olem1  13405  seqf1olem2  13406  znsqcld  13522  discr1  13596  hashnncl  13723  seqcoll2  13819  sqeqd  14517  sqrmo  14603  isercoll  15016  bitsfzo  15774  bitsinv1lem  15780  bitsf1  15785  bezoutlem3  15879  eucalglt  15919  phibndlem  16097  dfphi2  16101  prmdiv  16112  odzdvds  16122  pceq0  16197  pc2dvds  16205  fldivp1  16223  pcfac  16225  prmreclem3  16244  1arith  16253  4sqlem10  16273  4sqlem17  16287  4sqlem18  16288  vdwlem6  16312  ramubcl  16344  ramcl  16355  mrissmrcd  16903  psgnunilem5  18614  oddvdsnn0  18664  odnncl  18665  oddvds  18667  odcl2  18684  gexdvds  18701  gexnnod  18705  sylow1lem1  18715  odcau  18721  pgpssslw  18731  efgs1b  18854  efgredlema  18858  torsubg  18967  prmcyg  19007  gsumval3eu  19017  ablfacrplem  19180  ablfac1eu  19188  ablsimpgprmd  19230  lspdisj  19890  lspsncv0  19911  fidomndrnglem  20072  gzrngunitlem  20156  prmirredlem  20186  fctop  21609  cctop  21611  ppttop  21612  pptbas  21613  ordtrest2lem  21808  connclo  22020  txindis  22239  filconn  22488  ufilb  22511  cldsubg  22716  reconnlem1  23431  reconnlem2  23432  metds0  23455  metdseq0  23459  metnrmlem1a  23463  iccpnfhmeo  23550  xrhmeo  23551  cphsubrglem  23782  minveclem3b  24032  minveclem4a  24034  vitalilem4  24215  itg2gt0  24364  itgsplitioo  24441  limccnp2  24495  rollelem  24592  dvlip  24596  itgsubstlem  24651  plyaddlem1  24810  plymullem1  24811  coefv0  24845  dgreq0  24862  radcnv0  25011  pserdvlem2  25023  pilem2  25047  sineq0  25116  logtayl  25251  cxpsqrt  25294  isosctrlem2  25405  atantayl2  25524  rlimcnp2  25552  amgm  25576  basellem3  25668  muval2  25719  sqf11  25724  ppinprm  25737  chtnprm  25739  perfectlem2  25814  lgsdir  25916  lgsabs1  25920  lgseisenlem1  25959  2sqlem7  26008  2sqblem  26015  2sqmod  26020  2sqreultblem  26032  2sqreunnltblem  26035  chebbnd1lem1  26053  dchrisum0flblem1  26092  pntpbnd1  26170  pntpbnd2  26171  ostth  26223  symquadlem  26483  midexlem  26486  colperp  26523  midex  26531  oppperpex  26547  hlpasch  26550  hpgerlem  26559  colopp  26563  lmieu  26578  lmicom  26582  trgcopy  26598  cgracol  26622  minvecolem5  28664  staddi  30029  stadd3i  30031  atsseq  30130  atom1d  30136  atoml2i  30166  disji2f  30340  disjif2  30344  fprodex01  30567  psgnfzto1stlem  30792  lvecdim0  31093  ordtrest2NEWlem  31275  eulerpartlemb  31736  sgn3da  31909  subfacp1lem6  32542  cvmscld  32630  cvmsss2  32631  cvmseu  32633  nosepon  33282  ordtoplem  33893  ordcmp  33905  poimirlem25  35079  heiborlem6  35251  isfldidl  35503  pridlc2  35507  mpobi123f  35597  mptbi12f  35601  ac6s6  35607  lsatcmp  36296  lsatcmp2  36297  2atm  36820  trlatn0  37465  trlval3  37480  cdleme18c  37586  cdlemg17b  37955  cdlemg17i  37962  cdlemh  38110  dia2dimlem2  38358  dia2dimlem3  38359  dochlkr  38678  dochkrshp  38679  lcfl6  38793  lcfrlem9  38843  hdmap14lem6  39166  hgmapval0  39185  ioin9i8  39384  ctbnfien  39754  pw2f1ocnv  39973  unxpwdom3  40034  dgrsub2  40074  rp-fakeanorass  40216  mnuprdlem1  40975  mnuprdlem2  40976  mnurndlem1  40984  disjxp1  41698  fmul01lt1lem1  42221  elprn1  42270  stoweidlem35  42672  stirlinglem5  42715  stirlinglem12  42722  fourierdlem42  42786  fourierdlem93  42836  perfectALTVlem2  44235
  Copyright terms: Public domain W3C validator