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  878  po2nr  5622  po3nr  5623  ordn2lp  6415  ordnbtwn  6488  fpropnf1  7304  tfi  7890  nnlim  7917  frrlem14  8340  smoord  8421  tz7.48-3  8500  oalimcl  8616  omlimcl  8634  oneo  8637  omopth2  8640  nnneo  8711  sucdom2OLD  9148  mapdom2  9214  sucdom2  9269  php2  9274  php3OLD  9287  onomeneqOLD  9292  1sdom2dom  9310  isfinite2  9362  domunfican  9389  ordtypelem7  9593  unxpwdom2  9657  cantnfp1lem2  9748  oemapvali  9753  cantnflem1  9758  cantnflem2  9759  rankpwi  9892  tskwe  10019  alephordi  10143  alephdom  10150  cardaleph  10158  cflim2  10332  isfin4p1  10384  fin23lem26  10394  fin1a2lem13  10481  axcclem  10526  fpwwe2lem11  10710  fpwwe2lem12  10711  fpwwe2  10712  pwxpndom2  10734  pwxpndom  10735  pwdjundom  10736  gchaleph  10740  r1wunlim  10806  inatsk  10847  tskuni  10852  gruina  10887  prlem934  11102  dedekind  11453  prodge0rd  13164  qextltlem  13264  ixxub  13428  ixxlb  13429  seqf1olem1  14092  facndiv  14337  cnpart  15289  rlimuni  15596  rlimcld2  15624  isercoll  15716  incexclem  15884  isumltss  15896  alzdvds  16368  fzm1ndvds  16370  fzo0dvdseq  16371  bitsfzolem  16480  smuval2  16528  smupvallem  16529  bezoutlem3  16588  rpdvds  16707  nonsq  16806  prmdiv  16832  odzdvds  16842  pcprendvds  16887  pcprendvds2  16888  pcpremul  16890  pcdvdsb  16916  pcadd2  16937  pockthlem  16952  prmreclem5  16967  prmreclem6  16968  1arith  16974  4sqlem11  17002  vdwlem11  17038  vdwlem12  17039  ramubcl  17065  mrissmrcd  17698  pltnlt  18410  acsfiindd  18623  odcl2  19607  gexnnod  19630  pgpssslw  19656  torsubg  19896  lt6abl  19937  ablfacrplem  20109  pgpfac1lem3  20121  ablsimpnosubgd  20148  irredrmul  20453  islbs3  21180  lbsextlem3  21185  lbsextlem4  21186  f1lindf  21865  mvrf1  22029  psdmul  22193  perfopn  23214  pnfnei  23249  mnfnei  23250  haust1  23381  cmpcld  23431  ptbasfi  23610  fbncp  23868  isfild  23887  fbasfip  23897  filufint  23949  rnelfmlem  23981  fmfnfm  23987  fclscf  24054  ptcmplem3  24083  opnsubg  24137  bldisj  24429  iccntr  24862  icccmplem2  24864  reconnlem1  24867  reconnlem2  24868  evth  25010  lebnumlem3  25014  ovolicc2lem3  25573  volfiniun  25601  iundisj  25602  dvne0  26070  lhop2  26074  itgsubstlem  26109  coemullem  26309  plyexmo  26373  logccne0  26638  rtprmirr  26821  lgamgulmlem1  27090  wilthlem2  27130  wilth  27132  mumul  27242  chtublem  27273  perfect1  27290  lgsdilem2  27395  lgsne0  27397  lgsqrlem2  27409  lgseisenlem1  27437  lgseisenlem2  27438  lgsquadlem1  27442  lgsquadlem2  27443  lgsquadlem3  27444  lgsquad2lem1  27446  2sqblem  27493  chebbnd1lem1  27531  pntpbnd2  27649  pntlem3  27671  ostth  27701  sltval2  27719  nolt02o  27758  nosupbnd1lem2  27772  nosupbnd1  27777  nosupbnd2  27779  noinfbnd1lem2  27787  noinfbnd1  27792  noinfbnd2  27794  noetasuplem4  27799  noetainflem4  27803  scutbdaybnd2lim  27880  umgrnloop0  29144  usgrnloop0ALT  29240  wlkp1lem2  29710  pthdlem2lem  29803  chirredlem1  32422  iundisjf  32611  ofpreima2  32684  iundisjfi  32801  rprmndvdsru  33522  fundmpss  35730  dfon2lem4  35750  dfon2lem7  35753  broutsideof2  36086  outsidele  36096  nn0prpwlem  36288  onint1  36415  fin2so  37567  lindsadd  37573  lpssat  38969  exatleN  39361  3noncolr2  39406  4noncolr3  39410  3dimlem3  39418  3dimlem3OLDN  39419  3dimlem4a  39420  3dimlem4  39421  3dimlem4OLDN  39422  3atlem4  39443  3atlem5  39444  3atlem6  39445  llnnleat  39470  lplnnle2at  39498  lvolnle3at  39539  4atlem0a  39550  4atlem0ae  39551  dalem21  39651  dalem54  39683  cdlemblem  39750  lhpmcvr4N  39983  4atexlemnclw  40027  cdlemd3  40157  cdleme3g  40191  cdleme3h  40192  cdleme7aa  40199  cdleme7d  40203  cdleme7ga  40205  cdleme11c  40218  cdleme15b  40232  cdleme20zN  40258  cdleme21b  40283  cdleme21c  40284  cdleme21ct  40286  cdleme22b  40298  cdleme32b  40399  cdleme35fnpq  40406  cdleme35f  40411  cdleme36a  40417  cdleme42c  40429  cdleme48bw  40459  cdlemf1  40518  cdlemg2fv2  40557  cdlemg7fvbwN  40564  cdlemg4  40574  cdlemg6c  40577  cdlemg27a  40649  cdlemg27b  40653  cdlemk3  40790  dia2dimlem1  41021  dihord6apre  41213  dihord6b  41217  dihord5apre  41219  dihglbcpreN  41257  dihmeetlem6  41266  dochnel2  41349  dochexmidlem7  41423  lspindp5  41727  mapdh8b  41737  hdmapip0  41872  aks6d1c2p2  42076  flt4lem5elem  42606  flt4lem7  42614  nna4b4nsq  42615  pellexlem6  42790  elpell14qr2  42818  pellfundglb  42841  jm2.19  42950  jm2.26lem3  42958  setindtr  42981  harinf  42991  dgraa0p  43106  tfsconcatb0  43306  gneispace0nelrn3  44104