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  815  mtord  879  po2nr  5563  po3nr  5564  ordn2lp  6355  ordnbtwn  6430  fpropnf1  7245  tfi  7832  nnlim  7859  frrlem14  8281  smoord  8337  tz7.48-3  8415  oalimcl  8527  omlimcl  8545  oneo  8548  omopth2  8551  nnneo  8622  sucdom2OLD  9056  mapdom2  9118  sucdom2  9173  php2  9178  1sdom2dom  9201  isfinite2  9252  domunfican  9279  ordtypelem7  9484  unxpwdom2  9548  cantnfp1lem2  9639  oemapvali  9644  cantnflem1  9649  cantnflem2  9650  rankpwi  9783  tskwe  9910  alephordi  10034  alephdom  10041  cardaleph  10049  cflim2  10223  isfin4p1  10275  fin23lem26  10285  fin1a2lem13  10372  axcclem  10417  fpwwe2lem11  10601  fpwwe2lem12  10602  fpwwe2  10603  pwxpndom2  10625  pwxpndom  10626  pwdjundom  10627  gchaleph  10631  r1wunlim  10697  inatsk  10738  tskuni  10743  gruina  10778  prlem934  10993  dedekind  11344  prodge0rd  13067  qextltlem  13169  ixxub  13334  ixxlb  13335  seqf1olem1  14013  facndiv  14260  cnpart  15213  rlimuni  15523  rlimcld2  15551  isercoll  15641  incexclem  15809  isumltss  15821  alzdvds  16297  fzm1ndvds  16299  fzo0dvdseq  16300  bitsfzolem  16411  smuval2  16459  smupvallem  16460  bezoutlem3  16518  rpdvds  16637  nonsq  16736  prmdiv  16762  odzdvds  16773  pcprendvds  16818  pcprendvds2  16819  pcpremul  16821  pcdvdsb  16847  pcadd2  16868  pockthlem  16883  prmreclem5  16898  prmreclem6  16899  1arith  16905  4sqlem11  16933  vdwlem11  16969  vdwlem12  16970  ramubcl  16996  mrissmrcd  17608  pltnlt  18306  acsfiindd  18519  odcl2  19502  gexnnod  19525  pgpssslw  19551  torsubg  19791  lt6abl  19832  ablfacrplem  20004  pgpfac1lem3  20016  ablsimpnosubgd  20043  irredrmul  20343  islbs3  21072  lbsextlem3  21077  lbsextlem4  21078  f1lindf  21738  mvrf1  21902  psdmul  22060  perfopn  23079  pnfnei  23114  mnfnei  23115  haust1  23246  cmpcld  23296  ptbasfi  23475  fbncp  23733  isfild  23752  fbasfip  23762  filufint  23814  rnelfmlem  23846  fmfnfm  23852  fclscf  23919  ptcmplem3  23948  opnsubg  24002  bldisj  24293  iccntr  24717  icccmplem2  24719  reconnlem1  24722  reconnlem2  24723  evth  24865  lebnumlem3  24869  ovolicc2lem3  25427  volfiniun  25455  iundisj  25456  dvne0  25923  lhop2  25927  itgsubstlem  25962  coemullem  26162  plyexmo  26228  logccne0  26494  rtprmirr  26677  lgamgulmlem1  26946  wilthlem2  26986  wilth  26988  mumul  27098  chtublem  27129  perfect1  27146  lgsdilem2  27251  lgsne0  27253  lgsqrlem2  27265  lgseisenlem1  27293  lgseisenlem2  27294  lgsquadlem1  27298  lgsquadlem2  27299  lgsquadlem3  27300  lgsquad2lem1  27302  2sqblem  27349  chebbnd1lem1  27387  pntpbnd2  27505  pntlem3  27527  ostth  27557  sltval2  27575  nolt02o  27614  nosupbnd1lem2  27628  nosupbnd1  27633  nosupbnd2  27635  noinfbnd1lem2  27643  noinfbnd1  27648  noinfbnd2  27650  noetasuplem4  27655  noetainflem4  27659  scutbdaybnd2lim  27736  onsiso  28176  umgrnloop0  29043  usgrnloop0ALT  29139  wlkp1lem2  29609  pthdlem2lem  29704  chirredlem1  32326  iundisjf  32525  ofpreima2  32597  iundisjfi  32726  rprmndvdsru  33507  antnest  35683  antnestlaw3lem  35684  fundmpss  35761  dfon2lem4  35781  dfon2lem7  35784  broutsideof2  36117  outsidele  36127  nn0prpwlem  36317  onint1  36444  fin2so  37608  lindsadd  37614  lpssat  39013  exatleN  39405  3noncolr2  39450  4noncolr3  39454  3dimlem3  39462  3dimlem3OLDN  39463  3dimlem4a  39464  3dimlem4  39465  3dimlem4OLDN  39466  3atlem4  39487  3atlem5  39488  3atlem6  39489  llnnleat  39514  lplnnle2at  39542  lvolnle3at  39583  4atlem0a  39594  4atlem0ae  39595  dalem21  39695  dalem54  39727  cdlemblem  39794  lhpmcvr4N  40027  4atexlemnclw  40071  cdlemd3  40201  cdleme3g  40235  cdleme3h  40236  cdleme7aa  40243  cdleme7d  40247  cdleme7ga  40249  cdleme11c  40262  cdleme15b  40276  cdleme20zN  40302  cdleme21b  40327  cdleme21c  40328  cdleme21ct  40330  cdleme22b  40342  cdleme32b  40443  cdleme35fnpq  40450  cdleme35f  40455  cdleme36a  40461  cdleme42c  40473  cdleme48bw  40503  cdlemf1  40562  cdlemg2fv2  40601  cdlemg7fvbwN  40608  cdlemg4  40618  cdlemg6c  40621  cdlemg27a  40693  cdlemg27b  40697  cdlemk3  40834  dia2dimlem1  41065  dihord6apre  41257  dihord6b  41261  dihord5apre  41263  dihglbcpreN  41301  dihmeetlem6  41310  dochnel2  41393  dochexmidlem7  41467  lspindp5  41771  mapdh8b  41781  hdmapip0  41916  aks6d1c2p2  42114  flt4lem5elem  42646  flt4lem7  42654  nna4b4nsq  42655  pellexlem6  42829  elpell14qr2  42857  pellfundglb  42880  jm2.19  42989  jm2.26lem3  42997  setindtr  43020  harinf  43030  dgraa0p  43145  tfsconcatb0  43340  gneispace0nelrn3  44138