Theorem mtod 197

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 195	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  198  mtbid  324  mtbird  325  mtand  815  mtord  879  po2nr  5603  po3nr  5604  ordn2lp  6385  ordnbtwn  6458  fpropnf1  7266  tfi  7842  nnlim  7869  frrlem14  8284  smoord  8365  tz7.48-3  8444  oalimcl  8560  omlimcl  8578  oneo  8581  omopth2  8584  nnneo  8654  sucdom2OLD  9082  mapdom2  9148  sucdom2  9206  php2  9211  php3OLD  9224  onomeneqOLD  9229  1sdom2dom  9247  isfinite2  9301  domunfican  9320  ordtypelem7  9519  unxpwdom2  9583  cantnfp1lem2  9674  oemapvali  9679  cantnflem1  9684  cantnflem2  9685  rankpwi  9818  tskwe  9945  alephordi  10069  alephdom  10076  cardaleph  10084  cflim2  10258  isfin4p1  10310  fin23lem26  10320  fin1a2lem13  10407  axcclem  10452  fpwwe2lem11  10636  fpwwe2lem12  10637  fpwwe2  10638  pwxpndom2  10660  pwxpndom  10661  pwdjundom  10662  gchaleph  10666  r1wunlim  10732  inatsk  10773  tskuni  10778  gruina  10813  prlem934  11028  dedekind  11377  prodge0rd  13081  qextltlem  13181  ixxub  13345  ixxlb  13346  seqf1olem1  14007  facndiv  14248  cnpart  15187  rlimuni  15494  rlimcld2  15522  isercoll  15614  incexclem  15782  isumltss  15794  alzdvds  16263  fzm1ndvds  16265  fzo0dvdseq  16266  bitsfzolem  16375  smuval2  16423  smupvallem  16424  bezoutlem3  16483  rpdvds  16597  nonsq  16695  prmdiv  16718  odzdvds  16728  pcprendvds  16773  pcprendvds2  16774  pcpremul  16776  pcdvdsb  16802  pcadd2  16823  pockthlem  16838  prmreclem5  16853  prmreclem6  16854  1arith  16860  4sqlem11  16888  vdwlem11  16924  vdwlem12  16925  ramubcl  16951  mrissmrcd  17584  pltnlt  18293  acsfiindd  18506  odcl2  19433  gexnnod  19456  pgpssslw  19482  torsubg  19722  lt6abl  19763  ablfacrplem  19935  pgpfac1lem3  19947  ablsimpnosubgd  19974  irredrmul  20241  islbs3  20768  lbsextlem3  20773  lbsextlem4  20774  f1lindf  21377  mvrf1  21545  perfopn  22689  pnfnei  22724  mnfnei  22725  haust1  22856  cmpcld  22906  ptbasfi  23085  fbncp  23343  isfild  23362  fbasfip  23372  filufint  23424  rnelfmlem  23456  fmfnfm  23462  fclscf  23529  ptcmplem3  23558  opnsubg  23612  bldisj  23904  iccntr  24337  icccmplem2  24339  reconnlem1  24342  reconnlem2  24343  evth  24475  lebnumlem3  24479  ovolicc2lem3  25036  volfiniun  25064  iundisj  25065  dvne0  25528  lhop2  25532  itgsubstlem  25565  coemullem  25764  plyexmo  25826  logccne0  26087  lgamgulmlem1  26533  wilthlem2  26573  wilth  26575  mumul  26685  chtublem  26714  perfect1  26731  lgsdilem2  26836  lgsne0  26838  lgsqrlem2  26850  lgseisenlem1  26878  lgseisenlem2  26879  lgsquadlem1  26883  lgsquadlem2  26884  lgsquadlem3  26885  lgsquad2lem1  26887  2sqblem  26934  chebbnd1lem1  26972  pntpbnd2  27090  pntlem3  27112  ostth  27142  sltval2  27159  nolt02o  27198  nosupbnd1lem2  27212  nosupbnd1  27217  nosupbnd2  27219  noinfbnd1lem2  27227  noinfbnd1  27232  noinfbnd2  27234  noetasuplem4  27239  noetainflem4  27243  scutbdaybnd2lim  27318  umgrnloop0  28369  usgrnloop0ALT  28462  wlkp1lem2  28931  pthdlem2lem  29024  chirredlem1  31643  iundisjf  31820  ofpreima2  31891  iundisjfi  32007  fundmpss  34738  dfon2lem4  34758  dfon2lem7  34761  broutsideof2  35094  outsidele  35104  nn0prpwlem  35207  onint1  35334  fin2so  36475  lindsadd  36481  lpssat  37883  exatleN  38275  3noncolr2  38320  4noncolr3  38324  3dimlem3  38332  3dimlem3OLDN  38333  3dimlem4a  38334  3dimlem4  38335  3dimlem4OLDN  38336  3atlem4  38357  3atlem5  38358  3atlem6  38359  llnnleat  38384  lplnnle2at  38412  lvolnle3at  38453  4atlem0a  38464  4atlem0ae  38465  dalem21  38565  dalem54  38597  cdlemblem  38664  lhpmcvr4N  38897  4atexlemnclw  38941  cdlemd3  39071  cdleme3g  39105  cdleme3h  39106  cdleme7aa  39113  cdleme7d  39117  cdleme7ga  39119  cdleme11c  39132  cdleme15b  39146  cdleme20zN  39172  cdleme21b  39197  cdleme21c  39198  cdleme21ct  39200  cdleme22b  39212  cdleme32b  39313  cdleme35fnpq  39320  cdleme35f  39325  cdleme36a  39331  cdleme42c  39343  cdleme48bw  39373  cdlemf1  39432  cdlemg2fv2  39471  cdlemg7fvbwN  39478  cdlemg4  39488  cdlemg6c  39491  cdlemg27a  39563  cdlemg27b  39567  cdlemk3  39704  dia2dimlem1  39935  dihord6apre  40127  dihord6b  40131  dihord5apre  40133  dihglbcpreN  40171  dihmeetlem6  40180  dochnel2  40263  dochexmidlem7  40337  lspindp5  40641  mapdh8b  40651  hdmapip0  40786  aks6d1c2p2  40957  rtprmirr  41237  flt4lem5elem  41393  flt4lem7  41401  nna4b4nsq  41402  pellexlem6  41572  elpell14qr2  41600  pellfundglb  41623  jm2.19  41732  jm2.26lem3  41740  setindtr  41763  harinf  41773  dgraa0p  41891  tfsconcatb0  42094  gneispace0nelrn3  42893