Theorem mtod 201

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 26	. 2 ⊢ (𝜑 → (𝜓 → ¬ 𝜒))
4	1, 3	pm2.65d 199	1 ⊢ (𝜑 → ¬ 𝜓)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  mtoi  202  mtbid  327  mtbird  328  mtand  828  mtord  893  nrmod  3838  po2nr  5572  po3nr  5573  ordn2lp  6382  ordnbtwn  6458  fpropnf1  7271  tfi  7864  nnlim  7891  frrlem14  8320  smoord  8376  tz7.48-3  8457  oalimcl  8571  omlimcl  8589  oneo  8592  omopth2  8595  nnneo  8667  mapdom2  9170  sucdom2  9221  php2  9226  1sdom2dom  9248  isfinite2  9293  domunfican  9316  ordtypelem7  9521  unxpwdom2  9585  cantnfp1lem2  9683  oemapvali  9688  cantnflem1  9693  cantnflem2  9694  rankpwi  9835  tskwe  10034  alephordi  10156  alephdom  10163  cardaleph  10171  cflim2  10344  isfin4p1  10396  fin23lem26  10406  fin1a2lem13  10493  axcclem  10538  fpwwe2lem11  10729  fpwwe2lem12  10730  fpwwe2  10731  pwxpndom2  10753  pwxpndom  10754  pwdjundom  10755  gchaleph  10759  r1wunlim  10825  inatsk  10866  tskuni  10871  gruina  10906  prlem934  11121  dedekind  11476  prodge0rd  13232  qextltlem  13335  ixxub  13500  ixxlb  13501  seqf1olem1  14187  facndiv  14435  cnpart  15412  rlimuni  15722  rlimcld2  15750  isercoll  15840  incexclem  16010  isumltss  16022  alzdvds  16495  fzm1ndvds  16497  fzo0dvdseq  16498  bitsfzolem  16609  smuval2  16657  smupvallem  16658  bezoutlem3  16719  rpdvds  16840  nonsq  16940  prmdiv  16967  odzdvds  16978  pcprendvds  17023  pcprendvds2  17024  pcpremul  17026  pcdvdsb  17052  pcadd2  17073  pockthlem  17088  prmreclem5  17103  prmreclem6  17104  1arith  17110  4sqlem11  17138  vdwlem11  17174  vdwlem12  17175  ramubcl  17201  mrissmrcd  17819  pltnlt  18517  acsfiindd  18732  odcl2  19784  gexnnod  19807  pgpssslw  19833  torsubg  20073  lt6abl  20114  ablfacrplem  20286  pgpfac1lem3  20298  ablsimpnosubgd  20325  irredrmul  20662  islbs3  21438  lbsextlem3  21443  lbsextlem4  21444  f1lindf  22133  mvrf1  22298  psdmul  22492  perfopn  23508  pnfnei  23543  mnfnei  23544  haust1  23675  cmpcld  23725  ptbasfi  23905  fbncp  24163  isfild  24182  fbasfip  24192  filufint  24244  rnelfmlem  24276  fmfnfm  24282  fclscf  24349  ptcmplem3  24378  opnsubg  24432  bldisj  24722  iccntr  25146  icccmplem2  25148  reconnlem1  25151  reconnlem2  25152  evth  25285  lebnumlem3  25289  ovolicc2lem3  25845  volfiniun  25873  iundisj  25874  dvne0  26336  lhop2  26340  itgsubstlem  26373  coemullem  26574  rnplynfin  26635  plyexmo  26641  logccne0  26911  rtprmirr  27093  lgamgulmlem1  27361  wilthlem2  27401  wilth  27403  mumul  27513  chtublem  27543  perfect1  27560  lgsdilem2  27665  lgsne0  27667  lgsqrlem2  27679  lgseisenlem1  27707  lgseisenlem2  27708  lgsquadlem1  27712  lgsquadlem2  27713  lgsquadlem3  27714  lgsquad2lem1  27716  2sqblem  27763  chebbnd1lem1  27801  pntpbnd2  27919  pntlem3  27941  ostth  27971  flt4lem5elem  27986  flt4lem7  27994  nna4b4nsq  27995  ltsval2  28018  nolt02o  28057  nosupbnd1lem2  28071  nosupbnd1  28076  nosupbnd2  28078  noinfbnd1lem2  28086  noinfbnd1  28091  noinfbnd2  28093  noetasuplem4  28098  noetainflem4  28102  cutbdaybnd2lim  28188  oniso  28662  bdayfinbndlem1  28858  z12bdaylem1  28861  umgrnloop0  29692  usgrnloop0ALT  29791  wlkp1lem2  30258  pthdlem2lem  30358  chirredlem1  32997  iundisjf  33230  ofpreima2  33307  iundisjfi  33434  rprmndvdsru  34107  acwer1prc  35816  vonf1onprcf1ac  35963  onprcf1acwevd  35966  antnest  36540  antnestlaw3lem  36541  mirimanoffr  36546  fundmpss  36624  dfon2lem4  36640  dfon2lem7  36643  broutsideof2  36979  outsidele  36989  nn0prpwlem  37202  onint1  37329  fin2so  38623  lindsadd  38629  suceldisj  39843  lpssat  40163  exatleN  40554  3noncolr2  40599  4noncolr3  40603  3dimlem3  40611  3dimlem3OLDN  40612  3dimlem4a  40613  3dimlem4  40614  3dimlem4OLDN  40615  3atlem4  40636  3atlem5  40637  3atlem6  40638  llnnleat  40663  lplnnle2at  40691  lvolnle3at  40732  4atlem0a  40743  4atlem0ae  40744  dalem21  40844  dalem54  40876  cdlemblem  40943  lhpmcvr4N  41176  4atexlemnclw  41220  cdlemd3  41350  cdleme3g  41384  cdleme3h  41385  cdleme7aa  41392  cdleme7d  41396  cdleme7ga  41398  cdleme11c  41411  cdleme15b  41425  cdleme20zN  41451  cdleme21b  41476  cdleme21c  41477  cdleme21ct  41479  cdleme22b  41491  cdleme32b  41592  cdleme35fnpq  41599  cdleme35f  41604  cdleme36a  41610  cdleme42c  41622  cdleme48bw  41652  cdlemf1  41711  cdlemg2fv2  41750  cdlemg7fvbwN  41757  cdlemg4  41767  cdlemg6c  41770  cdlemg27a  41842  cdlemg27b  41846  cdlemk3  41983  dia2dimlem1  42214  dihord6apre  42406  dihord6b  42410  dihord5apre  42412  dihglbcpreN  42450  dihmeetlem6  42459  dochnel2  42542  dochexmidlem7  42616  lspindp5  42920  mapdh8b  42930  hdmapip0  43065  aks6d1c2p2  43262  pellexlem6  43934  elpell14qr2  43962  pellfundglb  43985  jm2.19  44093  jm2.26lem3  44101  setindtr  44124  harinf  44134  dgraa0p  44244  tfsconcatb0  44439  gneispace0nelrn3  45235  nellindf  51138