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  880  po2nr  5554  po3nr  5555  ordn2lp  6345  ordnbtwn  6420  fpropnf1  7223  tfi  7805  nnlim  7832  frrlem14  8251  smoord  8307  tz7.48-3  8385  oalimcl  8497  omlimcl  8515  oneo  8518  omopth2  8521  nnneo  8593  mapdom2  9088  sucdom2  9139  php2  9144  1sdom2dom  9166  isfinite2  9210  domunfican  9234  ordtypelem7  9441  unxpwdom2  9505  cantnfp1lem2  9600  oemapvali  9605  cantnflem1  9610  cantnflem2  9611  rankpwi  9747  tskwe  9874  alephordi  9996  alephdom  10003  cardaleph  10011  cflim2  10185  isfin4p1  10237  fin23lem26  10247  fin1a2lem13  10334  axcclem  10379  fpwwe2lem11  10564  fpwwe2lem12  10565  fpwwe2  10566  pwxpndom2  10588  pwxpndom  10589  pwdjundom  10590  gchaleph  10594  r1wunlim  10660  inatsk  10701  tskuni  10706  gruina  10741  prlem934  10956  dedekind  11308  prodge0rd  13026  qextltlem  13129  ixxub  13294  ixxlb  13295  seqf1olem1  13976  facndiv  14223  cnpart  15175  rlimuni  15485  rlimcld2  15513  isercoll  15603  incexclem  15771  isumltss  15783  alzdvds  16259  fzm1ndvds  16261  fzo0dvdseq  16262  bitsfzolem  16373  smuval2  16421  smupvallem  16422  bezoutlem3  16480  rpdvds  16599  nonsq  16698  prmdiv  16724  odzdvds  16735  pcprendvds  16780  pcprendvds2  16781  pcpremul  16783  pcdvdsb  16809  pcadd2  16830  pockthlem  16845  prmreclem5  16860  prmreclem6  16861  1arith  16867  4sqlem11  16895  vdwlem11  16931  vdwlem12  16932  ramubcl  16958  mrissmrcd  17575  pltnlt  18273  acsfiindd  18488  odcl2  19506  gexnnod  19529  pgpssslw  19555  torsubg  19795  lt6abl  19836  ablfacrplem  20008  pgpfac1lem3  20020  ablsimpnosubgd  20047  irredrmul  20375  islbs3  21122  lbsextlem3  21127  lbsextlem4  21128  f1lindf  21789  mvrf1  21953  psdmul  22121  perfopn  23141  pnfnei  23176  mnfnei  23177  haust1  23308  cmpcld  23358  ptbasfi  23537  fbncp  23795  isfild  23814  fbasfip  23824  filufint  23876  rnelfmlem  23908  fmfnfm  23914  fclscf  23981  ptcmplem3  24010  opnsubg  24064  bldisj  24354  iccntr  24778  icccmplem2  24780  reconnlem1  24783  reconnlem2  24784  evth  24926  lebnumlem3  24930  ovolicc2lem3  25488  volfiniun  25516  iundisj  25517  dvne0  25984  lhop2  25988  itgsubstlem  26023  coemullem  26223  plyexmo  26289  logccne0  26555  rtprmirr  26738  lgamgulmlem1  27007  wilthlem2  27047  wilth  27049  mumul  27159  chtublem  27190  perfect1  27207  lgsdilem2  27312  lgsne0  27314  lgsqrlem2  27326  lgseisenlem1  27354  lgseisenlem2  27355  lgsquadlem1  27359  lgsquadlem2  27360  lgsquadlem3  27361  lgsquad2lem1  27363  2sqblem  27410  chebbnd1lem1  27448  pntpbnd2  27566  pntlem3  27588  ostth  27618  ltsval2  27636  nolt02o  27675  nosupbnd1lem2  27689  nosupbnd1  27694  nosupbnd2  27696  noinfbnd1lem2  27704  noinfbnd1  27709  noinfbnd2  27711  noetasuplem4  27716  noetainflem4  27720  cutbdaybnd2lim  27805  oniso  28279  bdayfinbndlem1  28475  z12bdaylem1  28478  umgrnloop0  29194  usgrnloop0ALT  29290  wlkp1lem2  29758  pthdlem2lem  29852  chirredlem1  32477  iundisjf  32675  ofpreima2  32755  iundisjfi  32886  rprmndvdsru  33621  antnest  35902  antnestlaw3lem  35903  fundmpss  35980  dfon2lem4  35997  dfon2lem7  36000  broutsideof2  36335  outsidele  36345  nn0prpwlem  36535  onint1  36662  fin2so  37852  lindsadd  37858  suceldisj  39063  lpssat  39383  exatleN  39774  3noncolr2  39819  4noncolr3  39823  3dimlem3  39831  3dimlem3OLDN  39832  3dimlem4a  39833  3dimlem4  39834  3dimlem4OLDN  39835  3atlem4  39856  3atlem5  39857  3atlem6  39858  llnnleat  39883  lplnnle2at  39911  lvolnle3at  39952  4atlem0a  39963  4atlem0ae  39964  dalem21  40064  dalem54  40096  cdlemblem  40163  lhpmcvr4N  40396  4atexlemnclw  40440  cdlemd3  40570  cdleme3g  40604  cdleme3h  40605  cdleme7aa  40612  cdleme7d  40616  cdleme7ga  40618  cdleme11c  40631  cdleme15b  40645  cdleme20zN  40671  cdleme21b  40696  cdleme21c  40697  cdleme21ct  40699  cdleme22b  40711  cdleme32b  40812  cdleme35fnpq  40819  cdleme35f  40824  cdleme36a  40830  cdleme42c  40842  cdleme48bw  40872  cdlemf1  40931  cdlemg2fv2  40970  cdlemg7fvbwN  40977  cdlemg4  40987  cdlemg6c  40990  cdlemg27a  41062  cdlemg27b  41066  cdlemk3  41203  dia2dimlem1  41434  dihord6apre  41626  dihord6b  41630  dihord5apre  41632  dihglbcpreN  41670  dihmeetlem6  41679  dochnel2  41762  dochexmidlem7  41836  lspindp5  42140  mapdh8b  42150  hdmapip0  42285  aks6d1c2p2  42483  flt4lem5elem  43003  flt4lem7  43011  nna4b4nsq  43012  pellexlem6  43185  elpell14qr2  43213  pellfundglb  43236  jm2.19  43344  jm2.26lem3  43352  setindtr  43375  harinf  43385  dgraa0p  43500  tfsconcatb0  43695  gneispace0nelrn3  44492