Theorem mtod 200

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

Step	Hyp	Ref	Expression
1		mtod.2	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		mtod.1	. . 3 ⊢ (𝜑 → ¬ 𝜒)
3	2	a1d 25	. 2 ⊢ (𝜑 → (𝜓 → ¬ 𝜒))
4	1, 3	pm2.65d 198	1 ⊢ (𝜑 → ¬ 𝜓)

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  201  mtbid  326  mtbird  327  mtand  823  mtord  888  po2nr  5558  po3nr  5559  ordn2lp  6351  ordnbtwn  6426  fpropnf1  7236  tfi  7818  nnlim  7845  frrlem14  8264  smoord  8320  tz7.48-3  8399  oalimcl  8513  omlimcl  8531  oneo  8534  omopth2  8537  nnneo  8609  mapdom2  9105  sucdom2  9156  php2  9161  1sdom2dom  9183  isfinite2  9227  domunfican  9251  ordtypelem7  9458  unxpwdom2  9522  cantnfp1lem2  9620  oemapvali  9625  cantnflem1  9630  cantnflem2  9631  rankpwi  9767  tskwe  9894  alephordi  10016  alephdom  10023  cardaleph  10031  cflim2  10206  isfin4p1  10258  fin23lem26  10268  fin1a2lem13  10355  axcclem  10400  fpwwe2lem11  10585  fpwwe2lem12  10586  fpwwe2  10587  pwxpndom2  10609  pwxpndom  10610  pwdjundom  10611  gchaleph  10615  r1wunlim  10681  inatsk  10722  tskuni  10727  gruina  10762  prlem934  10977  dedekind  11332  prodge0rd  13088  qextltlem  13191  ixxub  13356  ixxlb  13357  seqf1olem1  14040  facndiv  14287  cnpart  15239  rlimuni  15549  rlimcld2  15577  isercoll  15667  incexclem  15838  isumltss  15850  alzdvds  16326  fzm1ndvds  16328  fzo0dvdseq  16329  bitsfzolem  16440  smuval2  16488  smupvallem  16489  bezoutlem3  16547  rpdvds  16666  nonsq  16766  prmdiv  16792  odzdvds  16803  pcprendvds  16848  pcprendvds2  16849  pcpremul  16851  pcdvdsb  16877  pcadd2  16898  pockthlem  16913  prmreclem5  16928  prmreclem6  16929  1arith  16935  4sqlem11  16963  vdwlem11  16999  vdwlem12  17000  ramubcl  17026  mrissmrcd  17644  pltnlt  18342  acsfiindd  18557  odcl2  19577  gexnnod  19600  pgpssslw  19626  torsubg  19866  lt6abl  19907  ablfacrplem  20079  pgpfac1lem3  20091  ablsimpnosubgd  20118  irredrmul  20444  islbs3  21194  lbsextlem3  21199  lbsextlem4  21200  f1lindf  21843  mvrf1  22006  psdmul  22200  perfopn  23214  pnfnei  23249  mnfnei  23250  haust1  23381  cmpcld  23431  ptbasfi  23610  fbncp  23868  isfild  23887  fbasfip  23897  filufint  23949  rnelfmlem  23981  fmfnfm  23987  fclscf  24054  ptcmplem3  24083  opnsubg  24137  bldisj  24427  iccntr  24851  icccmplem2  24853  reconnlem1  24856  reconnlem2  24857  evth  24990  lebnumlem3  24994  ovolicc2lem3  25550  volfiniun  25578  iundisj  25579  dvne0  26042  lhop2  26046  itgsubstlem  26079  coemullem  26279  plyexmo  26343  logccne0  26609  rtprmirr  26791  lgamgulmlem1  27059  wilthlem2  27099  wilth  27101  mumul  27211  chtublem  27241  perfect1  27258  lgsdilem2  27363  lgsne0  27365  lgsqrlem2  27377  lgseisenlem1  27405  lgseisenlem2  27406  lgsquadlem1  27410  lgsquadlem2  27411  lgsquadlem3  27412  lgsquad2lem1  27414  2sqblem  27461  chebbnd1lem1  27499  pntpbnd2  27617  pntlem3  27639  ostth  27669  ltsval2  27686  nolt02o  27725  nosupbnd1lem2  27739  nosupbnd1  27744  nosupbnd2  27746  noinfbnd1lem2  27754  noinfbnd1  27759  noinfbnd2  27761  noetasuplem4  27766  noetainflem4  27770  cutbdaybnd2lim  27856  oniso  28330  bdayfinbndlem1  28526  z12bdaylem1  28529  umgrnloop0  29245  usgrnloop0ALT  29341  wlkp1lem2  29808  pthdlem2lem  29902  chirredlem1  32528  iundisjf  32727  ofpreima2  32807  iundisjfi  32937  rprmndvdsru  33669  antnest  35977  antnestlaw3lem  35978  fundmpss  36055  dfon2lem4  36072  dfon2lem7  36075  broutsideof2  36410  outsidele  36420  nn0prpwlem  36620  onint1  36747  fin2so  38044  lindsadd  38050  suceldisj  39255  lpssat  39575  exatleN  39966  3noncolr2  40011  4noncolr3  40015  3dimlem3  40023  3dimlem3OLDN  40024  3dimlem4a  40025  3dimlem4  40026  3dimlem4OLDN  40027  3atlem4  40048  3atlem5  40049  3atlem6  40050  llnnleat  40075  lplnnle2at  40103  lvolnle3at  40144  4atlem0a  40155  4atlem0ae  40156  dalem21  40256  dalem54  40288  cdlemblem  40355  lhpmcvr4N  40588  4atexlemnclw  40632  cdlemd3  40762  cdleme3g  40796  cdleme3h  40797  cdleme7aa  40804  cdleme7d  40808  cdleme7ga  40810  cdleme11c  40823  cdleme15b  40837  cdleme20zN  40863  cdleme21b  40888  cdleme21c  40889  cdleme21ct  40891  cdleme22b  40903  cdleme32b  41004  cdleme35fnpq  41011  cdleme35f  41016  cdleme36a  41022  cdleme42c  41034  cdleme48bw  41064  cdlemf1  41123  cdlemg2fv2  41162  cdlemg7fvbwN  41169  cdlemg4  41179  cdlemg6c  41182  cdlemg27a  41254  cdlemg27b  41258  cdlemk3  41395  dia2dimlem1  41626  dihord6apre  41818  dihord6b  41822  dihord5apre  41824  dihglbcpreN  41862  dihmeetlem6  41871  dochnel2  41954  dochexmidlem7  42028  lspindp5  42332  mapdh8b  42342  hdmapip0  42477  aks6d1c2p2  42674  flt4lem5elem  43171  flt4lem7  43179  nna4b4nsq  43180  pellexlem6  43349  elpell14qr2  43377  pellfundglb  43400  jm2.19  43508  jm2.26lem3  43516  setindtr  43539  harinf  43549  dgraa0p  43664  tfsconcatb0  43859  gneispace0nelrn3  44656