Theorem mtod 198

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 196	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  199  mtbid  324  mtbird  325  mtand  816  mtord  879  po2nr  5610  po3nr  5611  ordn2lp  6405  ordnbtwn  6478  fpropnf1  7286  tfi  7873  nnlim  7900  frrlem14  8322  smoord  8403  tz7.48-3  8482  oalimcl  8596  omlimcl  8614  oneo  8617  omopth2  8620  nnneo  8691  sucdom2OLD  9120  mapdom2  9186  sucdom2  9240  php2  9245  php3OLD  9258  onomeneqOLD  9263  1sdom2dom  9280  isfinite2  9331  domunfican  9358  ordtypelem7  9561  unxpwdom2  9625  cantnfp1lem2  9716  oemapvali  9721  cantnflem1  9726  cantnflem2  9727  rankpwi  9860  tskwe  9987  alephordi  10111  alephdom  10118  cardaleph  10126  cflim2  10300  isfin4p1  10352  fin23lem26  10362  fin1a2lem13  10449  axcclem  10494  fpwwe2lem11  10678  fpwwe2lem12  10679  fpwwe2  10680  pwxpndom2  10702  pwxpndom  10703  pwdjundom  10704  gchaleph  10708  r1wunlim  10774  inatsk  10815  tskuni  10820  gruina  10855  prlem934  11070  dedekind  11421  prodge0rd  13139  qextltlem  13240  ixxub  13404  ixxlb  13405  seqf1olem1  14078  facndiv  14323  cnpart  15275  rlimuni  15582  rlimcld2  15610  isercoll  15700  incexclem  15868  isumltss  15880  alzdvds  16353  fzm1ndvds  16355  fzo0dvdseq  16356  bitsfzolem  16467  smuval2  16515  smupvallem  16516  bezoutlem3  16574  rpdvds  16693  nonsq  16792  prmdiv  16818  odzdvds  16828  pcprendvds  16873  pcprendvds2  16874  pcpremul  16876  pcdvdsb  16902  pcadd2  16923  pockthlem  16938  prmreclem5  16953  prmreclem6  16954  1arith  16960  4sqlem11  16988  vdwlem11  17024  vdwlem12  17025  ramubcl  17051  mrissmrcd  17684  pltnlt  18397  acsfiindd  18610  odcl2  19597  gexnnod  19620  pgpssslw  19646  torsubg  19886  lt6abl  19927  ablfacrplem  20099  pgpfac1lem3  20111  ablsimpnosubgd  20138  irredrmul  20443  islbs3  21174  lbsextlem3  21179  lbsextlem4  21180  f1lindf  21859  mvrf1  22023  psdmul  22187  perfopn  23208  pnfnei  23243  mnfnei  23244  haust1  23375  cmpcld  23425  ptbasfi  23604  fbncp  23862  isfild  23881  fbasfip  23891  filufint  23943  rnelfmlem  23975  fmfnfm  23981  fclscf  24048  ptcmplem3  24077  opnsubg  24131  bldisj  24423  iccntr  24856  icccmplem2  24858  reconnlem1  24861  reconnlem2  24862  evth  25004  lebnumlem3  25008  ovolicc2lem3  25567  volfiniun  25595  iundisj  25596  dvne0  26064  lhop2  26068  itgsubstlem  26103  coemullem  26303  plyexmo  26369  logccne0  26634  rtprmirr  26817  lgamgulmlem1  27086  wilthlem2  27126  wilth  27128  mumul  27238  chtublem  27269  perfect1  27286  lgsdilem2  27391  lgsne0  27393  lgsqrlem2  27405  lgseisenlem1  27433  lgseisenlem2  27434  lgsquadlem1  27438  lgsquadlem2  27439  lgsquadlem3  27440  lgsquad2lem1  27442  2sqblem  27489  chebbnd1lem1  27527  pntpbnd2  27645  pntlem3  27667  ostth  27697  sltval2  27715  nolt02o  27754  nosupbnd1lem2  27768  nosupbnd1  27773  nosupbnd2  27775  noinfbnd1lem2  27783  noinfbnd1  27788  noinfbnd2  27790  noetasuplem4  27795  noetainflem4  27799  scutbdaybnd2lim  27876  umgrnloop0  29140  usgrnloop0ALT  29236  wlkp1lem2  29706  pthdlem2lem  29799  chirredlem1  32418  iundisjf  32608  ofpreima2  32682  iundisjfi  32803  rprmndvdsru  33536  antnest  35673  fundmpss  35747  dfon2lem4  35767  dfon2lem7  35770  broutsideof2  36103  outsidele  36113  nn0prpwlem  36304  onint1  36431  fin2so  37593  lindsadd  37599  lpssat  38994  exatleN  39386  3noncolr2  39431  4noncolr3  39435  3dimlem3  39443  3dimlem3OLDN  39444  3dimlem4a  39445  3dimlem4  39446  3dimlem4OLDN  39447  3atlem4  39468  3atlem5  39469  3atlem6  39470  llnnleat  39495  lplnnle2at  39523  lvolnle3at  39564  4atlem0a  39575  4atlem0ae  39576  dalem21  39676  dalem54  39708  cdlemblem  39775  lhpmcvr4N  40008  4atexlemnclw  40052  cdlemd3  40182  cdleme3g  40216  cdleme3h  40217  cdleme7aa  40224  cdleme7d  40228  cdleme7ga  40230  cdleme11c  40243  cdleme15b  40257  cdleme20zN  40283  cdleme21b  40308  cdleme21c  40309  cdleme21ct  40311  cdleme22b  40323  cdleme32b  40424  cdleme35fnpq  40431  cdleme35f  40436  cdleme36a  40442  cdleme42c  40454  cdleme48bw  40484  cdlemf1  40543  cdlemg2fv2  40582  cdlemg7fvbwN  40589  cdlemg4  40599  cdlemg6c  40602  cdlemg27a  40674  cdlemg27b  40678  cdlemk3  40815  dia2dimlem1  41046  dihord6apre  41238  dihord6b  41242  dihord5apre  41244  dihglbcpreN  41282  dihmeetlem6  41291  dochnel2  41374  dochexmidlem7  41448  lspindp5  41752  mapdh8b  41762  hdmapip0  41897  aks6d1c2p2  42100  flt4lem5elem  42637  flt4lem7  42645  nna4b4nsq  42646  pellexlem6  42821  elpell14qr2  42849  pellfundglb  42872  jm2.19  42981  jm2.26lem3  42989  setindtr  43012  harinf  43022  dgraa0p  43137  tfsconcatb0  43333  gneispace0nelrn3  44131