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  5541  po3nr  5542  ordn2lp  6331  ordnbtwn  6406  fpropnf1  7207  tfi  7789  nnlim  7816  frrlem14  8235  smoord  8291  tz7.48-3  8369  oalimcl  8481  omlimcl  8499  oneo  8502  omopth2  8505  nnneo  8576  mapdom2  9068  sucdom2  9119  php2  9124  1sdom2dom  9145  isfinite2  9189  domunfican  9213  ordtypelem7  9417  unxpwdom2  9481  cantnfp1lem2  9576  oemapvali  9581  cantnflem1  9586  cantnflem2  9587  rankpwi  9723  tskwe  9850  alephordi  9972  alephdom  9979  cardaleph  9987  cflim2  10161  isfin4p1  10213  fin23lem26  10223  fin1a2lem13  10310  axcclem  10355  fpwwe2lem11  10539  fpwwe2lem12  10540  fpwwe2  10541  pwxpndom2  10563  pwxpndom  10564  pwdjundom  10565  gchaleph  10569  r1wunlim  10635  inatsk  10676  tskuni  10681  gruina  10716  prlem934  10931  dedekind  11283  prodge0rd  13001  qextltlem  13103  ixxub  13268  ixxlb  13269  seqf1olem1  13950  facndiv  14197  cnpart  15149  rlimuni  15459  rlimcld2  15487  isercoll  15577  incexclem  15745  isumltss  15757  alzdvds  16233  fzm1ndvds  16235  fzo0dvdseq  16236  bitsfzolem  16347  smuval2  16395  smupvallem  16396  bezoutlem3  16454  rpdvds  16573  nonsq  16672  prmdiv  16698  odzdvds  16709  pcprendvds  16754  pcprendvds2  16755  pcpremul  16757  pcdvdsb  16783  pcadd2  16804  pockthlem  16819  prmreclem5  16834  prmreclem6  16835  1arith  16841  4sqlem11  16869  vdwlem11  16905  vdwlem12  16906  ramubcl  16932  mrissmrcd  17548  pltnlt  18246  acsfiindd  18461  odcl2  19479  gexnnod  19502  pgpssslw  19528  torsubg  19768  lt6abl  19809  ablfacrplem  19981  pgpfac1lem3  19993  ablsimpnosubgd  20020  irredrmul  20347  islbs3  21094  lbsextlem3  21099  lbsextlem4  21100  f1lindf  21761  mvrf1  21924  psdmul  22082  perfopn  23101  pnfnei  23136  mnfnei  23137  haust1  23268  cmpcld  23318  ptbasfi  23497  fbncp  23755  isfild  23774  fbasfip  23784  filufint  23836  rnelfmlem  23868  fmfnfm  23874  fclscf  23941  ptcmplem3  23970  opnsubg  24024  bldisj  24314  iccntr  24738  icccmplem2  24740  reconnlem1  24743  reconnlem2  24744  evth  24886  lebnumlem3  24890  ovolicc2lem3  25448  volfiniun  25476  iundisj  25477  dvne0  25944  lhop2  25948  itgsubstlem  25983  coemullem  26183  plyexmo  26249  logccne0  26515  rtprmirr  26698  lgamgulmlem1  26967  wilthlem2  27007  wilth  27009  mumul  27119  chtublem  27150  perfect1  27167  lgsdilem2  27272  lgsne0  27274  lgsqrlem2  27286  lgseisenlem1  27314  lgseisenlem2  27315  lgsquadlem1  27319  lgsquadlem2  27320  lgsquadlem3  27321  lgsquad2lem1  27323  2sqblem  27370  chebbnd1lem1  27408  pntpbnd2  27526  pntlem3  27548  ostth  27578  sltval2  27596  nolt02o  27635  nosupbnd1lem2  27649  nosupbnd1  27654  nosupbnd2  27656  noinfbnd1lem2  27664  noinfbnd1  27669  noinfbnd2  27671  noetasuplem4  27676  noetainflem4  27680  scutbdaybnd2lim  27759  onsiso  28206  umgrnloop0  29089  usgrnloop0ALT  29185  wlkp1lem2  29653  pthdlem2lem  29747  chirredlem1  32372  iundisjf  32571  ofpreima2  32650  iundisjfi  32783  rprmndvdsru  33501  antnest  35754  antnestlaw3lem  35755  fundmpss  35832  dfon2lem4  35849  dfon2lem7  35852  broutsideof2  36187  outsidele  36197  nn0prpwlem  36387  onint1  36514  fin2so  37667  lindsadd  37673  lpssat  39132  exatleN  39523  3noncolr2  39568  4noncolr3  39572  3dimlem3  39580  3dimlem3OLDN  39581  3dimlem4a  39582  3dimlem4  39583  3dimlem4OLDN  39584  3atlem4  39605  3atlem5  39606  3atlem6  39607  llnnleat  39632  lplnnle2at  39660  lvolnle3at  39701  4atlem0a  39712  4atlem0ae  39713  dalem21  39813  dalem54  39845  cdlemblem  39912  lhpmcvr4N  40145  4atexlemnclw  40189  cdlemd3  40319  cdleme3g  40353  cdleme3h  40354  cdleme7aa  40361  cdleme7d  40365  cdleme7ga  40367  cdleme11c  40380  cdleme15b  40394  cdleme20zN  40420  cdleme21b  40445  cdleme21c  40446  cdleme21ct  40448  cdleme22b  40460  cdleme32b  40561  cdleme35fnpq  40568  cdleme35f  40573  cdleme36a  40579  cdleme42c  40591  cdleme48bw  40621  cdlemf1  40680  cdlemg2fv2  40719  cdlemg7fvbwN  40726  cdlemg4  40736  cdlemg6c  40739  cdlemg27a  40811  cdlemg27b  40815  cdlemk3  40952  dia2dimlem1  41183  dihord6apre  41375  dihord6b  41379  dihord5apre  41381  dihglbcpreN  41419  dihmeetlem6  41428  dochnel2  41511  dochexmidlem7  41585  lspindp5  41889  mapdh8b  41899  hdmapip0  42034  aks6d1c2p2  42232  flt4lem5elem  42769  flt4lem7  42777  nna4b4nsq  42778  pellexlem6  42951  elpell14qr2  42979  pellfundglb  43002  jm2.19  43110  jm2.26lem3  43118  setindtr  43141  harinf  43151  dgraa0p  43266  tfsconcatb0  43461  gneispace0nelrn3  44259