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  5606  po3nr  5607  ordn2lp  6404  ordnbtwn  6477  fpropnf1  7287  tfi  7874  nnlim  7901  frrlem14  8324  smoord  8405  tz7.48-3  8484  oalimcl  8598  omlimcl  8616  oneo  8619  omopth2  8622  nnneo  8693  sucdom2OLD  9122  mapdom2  9188  sucdom2  9243  php2  9248  php3OLD  9261  onomeneqOLD  9266  1sdom2dom  9283  isfinite2  9334  domunfican  9361  ordtypelem7  9564  unxpwdom2  9628  cantnfp1lem2  9719  oemapvali  9724  cantnflem1  9729  cantnflem2  9730  rankpwi  9863  tskwe  9990  alephordi  10114  alephdom  10121  cardaleph  10129  cflim2  10303  isfin4p1  10355  fin23lem26  10365  fin1a2lem13  10452  axcclem  10497  fpwwe2lem11  10681  fpwwe2lem12  10682  fpwwe2  10683  pwxpndom2  10705  pwxpndom  10706  pwdjundom  10707  gchaleph  10711  r1wunlim  10777  inatsk  10818  tskuni  10823  gruina  10858  prlem934  11073  dedekind  11424  prodge0rd  13142  qextltlem  13244  ixxub  13408  ixxlb  13409  seqf1olem1  14082  facndiv  14327  cnpart  15279  rlimuni  15586  rlimcld2  15614  isercoll  15704  incexclem  15872  isumltss  15884  alzdvds  16357  fzm1ndvds  16359  fzo0dvdseq  16360  bitsfzolem  16471  smuval2  16519  smupvallem  16520  bezoutlem3  16578  rpdvds  16697  nonsq  16796  prmdiv  16822  odzdvds  16833  pcprendvds  16878  pcprendvds2  16879  pcpremul  16881  pcdvdsb  16907  pcadd2  16928  pockthlem  16943  prmreclem5  16958  prmreclem6  16959  1arith  16965  4sqlem11  16993  vdwlem11  17029  vdwlem12  17030  ramubcl  17056  mrissmrcd  17683  pltnlt  18385  acsfiindd  18598  odcl2  19583  gexnnod  19606  pgpssslw  19632  torsubg  19872  lt6abl  19913  ablfacrplem  20085  pgpfac1lem3  20097  ablsimpnosubgd  20124  irredrmul  20427  islbs3  21157  lbsextlem3  21162  lbsextlem4  21163  f1lindf  21842  mvrf1  22006  psdmul  22170  perfopn  23193  pnfnei  23228  mnfnei  23229  haust1  23360  cmpcld  23410  ptbasfi  23589  fbncp  23847  isfild  23866  fbasfip  23876  filufint  23928  rnelfmlem  23960  fmfnfm  23966  fclscf  24033  ptcmplem3  24062  opnsubg  24116  bldisj  24408  iccntr  24843  icccmplem2  24845  reconnlem1  24848  reconnlem2  24849  evth  24991  lebnumlem3  24995  ovolicc2lem3  25554  volfiniun  25582  iundisj  25583  dvne0  26050  lhop2  26054  itgsubstlem  26089  coemullem  26289  plyexmo  26355  logccne0  26620  rtprmirr  26803  lgamgulmlem1  27072  wilthlem2  27112  wilth  27114  mumul  27224  chtublem  27255  perfect1  27272  lgsdilem2  27377  lgsne0  27379  lgsqrlem2  27391  lgseisenlem1  27419  lgseisenlem2  27420  lgsquadlem1  27424  lgsquadlem2  27425  lgsquadlem3  27426  lgsquad2lem1  27428  2sqblem  27475  chebbnd1lem1  27513  pntpbnd2  27631  pntlem3  27653  ostth  27683  sltval2  27701  nolt02o  27740  nosupbnd1lem2  27754  nosupbnd1  27759  nosupbnd2  27761  noinfbnd1lem2  27769  noinfbnd1  27774  noinfbnd2  27776  noetasuplem4  27781  noetainflem4  27785  scutbdaybnd2lim  27862  umgrnloop0  29126  usgrnloop0ALT  29222  wlkp1lem2  29692  pthdlem2lem  29787  chirredlem1  32409  iundisjf  32602  ofpreima2  32676  iundisjfi  32798  rprmndvdsru  33557  antnest  35694  fundmpss  35767  dfon2lem4  35787  dfon2lem7  35790  broutsideof2  36123  outsidele  36133  nn0prpwlem  36323  onint1  36450  fin2so  37614  lindsadd  37620  lpssat  39014  exatleN  39406  3noncolr2  39451  4noncolr3  39455  3dimlem3  39463  3dimlem3OLDN  39464  3dimlem4a  39465  3dimlem4  39466  3dimlem4OLDN  39467  3atlem4  39488  3atlem5  39489  3atlem6  39490  llnnleat  39515  lplnnle2at  39543  lvolnle3at  39584  4atlem0a  39595  4atlem0ae  39596  dalem21  39696  dalem54  39728  cdlemblem  39795  lhpmcvr4N  40028  4atexlemnclw  40072  cdlemd3  40202  cdleme3g  40236  cdleme3h  40237  cdleme7aa  40244  cdleme7d  40248  cdleme7ga  40250  cdleme11c  40263  cdleme15b  40277  cdleme20zN  40303  cdleme21b  40328  cdleme21c  40329  cdleme21ct  40331  cdleme22b  40343  cdleme32b  40444  cdleme35fnpq  40451  cdleme35f  40456  cdleme36a  40462  cdleme42c  40474  cdleme48bw  40504  cdlemf1  40563  cdlemg2fv2  40602  cdlemg7fvbwN  40609  cdlemg4  40619  cdlemg6c  40622  cdlemg27a  40694  cdlemg27b  40698  cdlemk3  40835  dia2dimlem1  41066  dihord6apre  41258  dihord6b  41262  dihord5apre  41264  dihglbcpreN  41302  dihmeetlem6  41311  dochnel2  41394  dochexmidlem7  41468  lspindp5  41772  mapdh8b  41782  hdmapip0  41917  aks6d1c2p2  42120  flt4lem5elem  42661  flt4lem7  42669  nna4b4nsq  42670  pellexlem6  42845  elpell14qr2  42873  pellfundglb  42896  jm2.19  43005  jm2.26lem3  43013  setindtr  43036  harinf  43046  dgraa0p  43161  tfsconcatb0  43357  gneispace0nelrn3  44155