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 ⊢ (𝜑 → ¬ 𝜓)

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  202  mtbid  327  mtbird  328  mtand  827  mtord  892  po2nr  5574  po3nr  5575  ordn2lp  6370  ordnbtwn  6445  fpropnf1  7255  tfi  7837  nnlim  7864  frrlem14  8284  smoord  8340  tz7.48-3  8419  oalimcl  8533  omlimcl  8551  oneo  8554  omopth2  8557  nnneo  8629  mapdom2  9124  sucdom2  9175  php2  9180  1sdom2dom  9202  isfinite2  9246  domunfican  9269  ordtypelem7  9474  unxpwdom2  9538  cantnfp1lem2  9636  oemapvali  9641  cantnflem1  9646  cantnflem2  9647  rankpwi  9783  tskwe  9924  alephordi  10046  alephdom  10053  cardaleph  10061  cflim2  10235  isfin4p1  10287  fin23lem26  10297  fin1a2lem13  10384  axcclem  10429  fpwwe2lem11  10614  fpwwe2lem12  10615  fpwwe2  10616  pwxpndom2  10638  pwxpndom  10639  pwdjundom  10640  gchaleph  10644  r1wunlim  10710  inatsk  10751  tskuni  10756  gruina  10791  prlem934  11006  dedekind  11361  prodge0rd  13116  qextltlem  13219  ixxub  13384  ixxlb  13385  seqf1olem1  14068  facndiv  14315  cnpart  15281  rlimuni  15591  rlimcld2  15619  isercoll  15709  incexclem  15880  isumltss  15892  alzdvds  16368  fzm1ndvds  16370  fzo0dvdseq  16371  bitsfzolem  16482  smuval2  16530  smupvallem  16531  bezoutlem3  16589  rpdvds  16708  nonsq  16808  prmdiv  16834  odzdvds  16845  pcprendvds  16890  pcprendvds2  16891  pcpremul  16893  pcdvdsb  16919  pcadd2  16940  pockthlem  16955  prmreclem5  16970  prmreclem6  16971  1arith  16977  4sqlem11  17005  vdwlem11  17041  vdwlem12  17042  ramubcl  17068  mrissmrcd  17686  pltnlt  18384  acsfiindd  18599  odcl2  19626  gexnnod  19649  pgpssslw  19675  torsubg  19915  lt6abl  19956  ablfacrplem  20128  pgpfac1lem3  20140  ablsimpnosubgd  20167  irredrmul  20500  islbs3  21248  lbsextlem3  21253  lbsextlem4  21254  f1lindf  21932  mvrf1  22095  psdmul  22289  perfopn  23303  pnfnei  23338  mnfnei  23339  haust1  23470  cmpcld  23520  ptbasfi  23699  fbncp  23957  isfild  23976  fbasfip  23986  filufint  24038  rnelfmlem  24070  fmfnfm  24076  fclscf  24143  ptcmplem3  24172  opnsubg  24226  bldisj  24516  iccntr  24940  icccmplem2  24942  reconnlem1  24945  reconnlem2  24946  evth  25079  lebnumlem3  25083  ovolicc2lem3  25639  volfiniun  25667  iundisj  25668  dvne0  26131  lhop2  26135  itgsubstlem  26168  coemullem  26368  plyexmo  26435  logccne0  26701  rtprmirr  26883  lgamgulmlem1  27151  wilthlem2  27191  wilth  27193  mumul  27303  chtublem  27333  perfect1  27350  lgsdilem2  27455  lgsne0  27457  lgsqrlem2  27469  lgseisenlem1  27497  lgseisenlem2  27498  lgsquadlem1  27502  lgsquadlem2  27503  lgsquadlem3  27504  lgsquad2lem1  27506  2sqblem  27553  chebbnd1lem1  27591  pntpbnd2  27709  pntlem3  27731  ostth  27761  ltsval2  27778  nolt02o  27817  nosupbnd1lem2  27831  nosupbnd1  27836  nosupbnd2  27838  noinfbnd1lem2  27846  noinfbnd1  27851  noinfbnd2  27853  noetasuplem4  27858  noetainflem4  27862  cutbdaybnd2lim  27948  oniso  28422  bdayfinbndlem1  28618  z12bdaylem1  28621  umgrnloop0  29368  usgrnloop0ALT  29464  wlkp1lem2  29931  pthdlem2lem  30025  chirredlem1  32651  iundisjf  32844  ofpreima2  32923  iundisjfi  33053  rprmndvdsru  33736  antnest  36052  antnestlaw3lem  36053  fundmpss  36130  dfon2lem4  36147  dfon2lem7  36150  broutsideof2  36485  outsidele  36495  nn0prpwlem  36695  onint1  36822  fin2so  38118  lindsadd  38124  suceldisj  39329  lpssat  39649  exatleN  40040  3noncolr2  40085  4noncolr3  40089  3dimlem3  40097  3dimlem3OLDN  40098  3dimlem4a  40099  3dimlem4  40100  3dimlem4OLDN  40101  3atlem4  40122  3atlem5  40123  3atlem6  40124  llnnleat  40149  lplnnle2at  40177  lvolnle3at  40218  4atlem0a  40229  4atlem0ae  40230  dalem21  40330  dalem54  40362  cdlemblem  40429  lhpmcvr4N  40662  4atexlemnclw  40706  cdlemd3  40836  cdleme3g  40870  cdleme3h  40871  cdleme7aa  40878  cdleme7d  40882  cdleme7ga  40884  cdleme11c  40897  cdleme15b  40911  cdleme20zN  40937  cdleme21b  40962  cdleme21c  40963  cdleme21ct  40965  cdleme22b  40977  cdleme32b  41078  cdleme35fnpq  41085  cdleme35f  41090  cdleme36a  41096  cdleme42c  41108  cdleme48bw  41138  cdlemf1  41197  cdlemg2fv2  41236  cdlemg7fvbwN  41243  cdlemg4  41253  cdlemg6c  41256  cdlemg27a  41328  cdlemg27b  41332  cdlemk3  41469  dia2dimlem1  41700  dihord6apre  41892  dihord6b  41896  dihord5apre  41898  dihglbcpreN  41936  dihmeetlem6  41945  dochnel2  42028  dochexmidlem7  42102  lspindp5  42406  mapdh8b  42416  hdmapip0  42551  aks6d1c2p2  42748  flt4lem5elem  43245  flt4lem7  43253  nna4b4nsq  43254  pellexlem6  43423  elpell14qr2  43451  pellfundglb  43474  jm2.19  43582  jm2.26lem3  43590  setindtr  43613  harinf  43623  dgraa0p  43738  tfsconcatb0  43933  gneispace0nelrn3  44730