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

Theorem mtod 189
Description: Modus tollens deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)
Hypotheses
Ref Expression
mtod.1 (𝜑 → ¬ 𝜒)
mtod.2 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
mtod (𝜑 → ¬ 𝜓)

Proof of Theorem mtod
StepHypRef Expression
1 mtod.2 . 2 (𝜑 → (𝜓𝜒))
2 mtod.1 . . 3 (𝜑 → ¬ 𝜒)
32a1d 25 . 2 (𝜑 → (𝜓 → ¬ 𝜒))
41, 3pm2.65d 187 1 (𝜑 → ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem is referenced by:  mtoi  190  mtbid  313  mtbird  314  mtand  692  mtord  693  po2nr  5077  po3nr  5078  ordn2lp  5781  ordnbtwn  5854  fpropnf1  6564  tfi  7095  nnlim  7120  smoord  7507  tz7.48-3  7584  oalimcl  7685  omlimcl  7703  oneo  7706  omopth2  7709  nnneo  7776  mapdom2  8172  php3  8187  onomeneq  8191  sucdom2  8197  isfinite2  8259  domunfican  8274  ordtypelem7  8470  unxpwdom2  8534  cantnfp1lem2  8614  oemapvali  8619  cantnflem1  8624  cantnflem2  8625  rankpwi  8724  tskwe  8814  alephordi  8935  alephdom  8942  cardaleph  8950  cflim2  9123  isfin4-3  9175  fin23lem26  9185  fin1a2lem13  9272  axcclem  9317  fpwwe2lem12  9501  fpwwe2lem13  9502  fpwwe2  9503  pwxpndom2  9525  pwxpndom  9526  pwcdandom  9527  gchaleph  9531  r1wunlim  9597  inatsk  9638  tskuni  9643  gruina  9678  prlem934  9893  dedekind  10238  qextltlem  12071  ixxub  12234  ixxlb  12235  seqf1olem1  12880  facndiv  13115  cnpart  14024  rlimuni  14325  rlimcld2  14353  isercoll  14442  incexclem  14612  isumltss  14624  alzdvds  15089  fzm1ndvds  15091  fzo0dvdseq  15092  bitsfzolem  15203  smuval2  15251  smupvallem  15252  bezoutlem3  15305  rpdvds  15421  nonsq  15514  prmdiv  15537  odzdvds  15547  pcprendvds  15592  pcprendvds2  15593  pcpremul  15595  pcdvdsb  15620  pcadd2  15641  pockthlem  15656  prmreclem5  15671  prmreclem6  15672  1arith  15678  4sqlem11  15706  vdwlem11  15742  vdwlem12  15743  ramubcl  15769  mrissmrcd  16347  pltnlt  17015  acsfiindd  17224  odcl2  18028  gexnnod  18049  pgpssslw  18075  torsubg  18303  lt6abl  18342  ablfacrplem  18510  pgpfac1lem3  18522  irredrmul  18753  islbs3  19203  lbsextlem3  19208  lbsextlem4  19209  rng1nfld  19326  mvrf1  19473  f1lindf  20209  perfopn  21037  pnfnei  21072  mnfnei  21073  haust1  21204  cmpcld  21253  ptbasfi  21432  fbncp  21690  isfild  21709  fbasfip  21719  filufint  21771  rnelfmlem  21803  fmfnfm  21809  fclscf  21876  ptcmplem3  21905  opnsubg  21958  bldisj  22250  iccntr  22671  icccmplem2  22673  reconnlem1  22676  reconnlem2  22677  evth  22805  lebnumlem3  22809  ovolicc2lem3  23333  volfiniun  23361  iundisj  23362  dvne0  23819  lhop2  23823  itgsubstlem  23856  coemullem  24051  plyexmo  24113  logccne0  24370  lgamgulmlem1  24800  wilthlem2  24840  wilth  24842  mumul  24952  chtublem  24981  perfect1  24998  lgsdilem2  25103  lgsne0  25105  lgsqrlem2  25117  lgseisenlem1  25145  lgseisenlem2  25146  lgsquadlem1  25150  lgsquadlem2  25151  lgsquadlem3  25152  lgsquad2lem1  25154  2sqblem  25201  chebbnd1lem1  25203  pntpbnd2  25321  pntlem3  25343  ostth  25373  umgrnloop0  26049  usgrnloop0ALT  26142  wlkp1lem2  26627  pthdlem2lem  26719  chirredlem1  29377  iundisjf  29528  ofpreima2  29594  iundisjfi  29683  fundmpss  31790  dfon2lem4  31815  dfon2lem7  31818  sltval2  31934  nolt02o  31970  nosupbnd1lem2  31980  nosupbnd1  31985  nosupbnd2  31987  noetalem3  31990  broutsideof2  32354  outsidele  32364  nn0prpwlem  32442  nn0prpw  32443  onint1  32573  fin2so  33526  poimirlem16  33555  lpssat  34618  exatleN  35008  3noncolr2  35053  4noncolr3  35057  3dimlem3  35065  3dimlem3OLDN  35066  3dimlem4a  35067  3dimlem4  35068  3dimlem4OLDN  35069  3atlem4  35090  3atlem5  35091  3atlem6  35092  llnnleat  35117  lplnnle2at  35145  lvolnle3at  35186  4atlem0a  35197  4atlem0ae  35198  dalem21  35298  dalem54  35330  cdlemblem  35397  lhpmcvr4N  35630  4atexlemnclw  35674  cdlemd3  35805  cdleme3g  35839  cdleme3h  35840  cdleme7aa  35847  cdleme7d  35851  cdleme7ga  35853  cdleme11c  35866  cdleme15b  35880  cdleme20zN  35906  cdleme21b  35931  cdleme21c  35932  cdleme21ct  35934  cdleme22b  35946  cdleme32b  36047  cdleme35fnpq  36054  cdleme35f  36059  cdleme36a  36065  cdleme42c  36077  cdleme48bw  36107  cdlemf1  36166  cdlemg2fv2  36205  cdlemg7fvbwN  36212  cdlemg4  36222  cdlemg6c  36225  cdlemg27a  36297  cdlemg27b  36301  cdlemk3  36438  dia2dimlem1  36670  dihord6apre  36862  dihord6b  36866  dihord5apre  36868  dihglbcpreN  36906  dihmeetlem6  36915  dochnel2  36998  dochexmidlem7  37072  lspindp5  37376  mapdh8b  37386  hdmapip0  37524  pellexlem6  37715  elpell14qr2  37743  pellfundglb  37766  jm2.19  37877  jm2.26lem3  37885  setindtr  37908  harinf  37918  dgraa0p  38036  gneispace0nelrn3  38757
  Copyright terms: Public domain W3C validator