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  3843  po2nr  5577  po3nr  5578  ordn2lp  6400  ordnbtwn  6476  fpropnf1  7294  tfi  7888  nnlim  7915  frrlem14  8345  smoord  8401  tz7.48-3  8482  oalimcl  8596  omlimcl  8614  oneo  8617  omopth2  8620  nnneo  8692  mapdom2  9195  sucdom2  9246  php2  9251  1sdom2dom  9273  isfinite2  9318  domunfican  9341  ordtypelem7  9545  unxpwdom2  9609  cantnfp1lem2  9707  oemapvali  9712  cantnflem1  9717  cantnflem2  9718  rankpwi  9859  tskwe  10058  alephordi  10180  alephdom  10187  cardaleph  10195  cflim2  10368  isfin4p1  10420  fin23lem26  10430  fin1a2lem13  10517  axcclem  10562  fpwwe2lem11  10753  fpwwe2lem12  10754  fpwwe2  10755  pwxpndom2  10777  pwxpndom  10778  pwdjundom  10779  gchaleph  10783  r1wunlim  10849  inatsk  10890  tskuni  10895  gruina  10930  prlem934  11145  dedekind  11500  prodge0rd  13256  qextltlem  13359  ixxub  13524  ixxlb  13525  seqf1olem1  14211  facndiv  14459  cnpart  15436  rlimuni  15746  rlimcld2  15774  isercoll  15864  incexclem  16034  isumltss  16046  alzdvds  16519  fzm1ndvds  16521  fzo0dvdseq  16522  bitsfzolem  16633  smuval2  16681  smupvallem  16682  bezoutlem3  16743  rpdvds  16864  nonsq  16964  prmdiv  16991  odzdvds  17002  pcprendvds  17047  pcprendvds2  17048  pcpremul  17050  pcdvdsb  17076  pcadd2  17097  pockthlem  17112  prmreclem5  17127  prmreclem6  17128  1arith  17134  4sqlem11  17162  vdwlem11  17198  vdwlem12  17199  ramubcl  17225  mrissmrcd  17843  pltnlt  18541  acsfiindd  18756  odcl2  19809  gexnnod  19832  pgpssslw  19858  torsubg  20098  lt6abl  20139  ablfacrplem  20311  pgpfac1lem3  20323  ablsimpnosubgd  20350  irredrmul  20687  islbs3  21463  lbsextlem3  21468  lbsextlem4  21469  f1lindf  22158  mvrf1  22323  psdmul  22517  perfopn  23533  pnfnei  23568  mnfnei  23569  haust1  23700  cmpcld  23750  ptbasfi  23930  fbncp  24188  isfild  24207  fbasfip  24217  filufint  24269  rnelfmlem  24301  fmfnfm  24307  fclscf  24374  ptcmplem3  24403  opnsubg  24457  bldisj  24747  iccntr  25171  icccmplem2  25173  reconnlem1  25176  reconnlem2  25177  evth  25310  lebnumlem3  25314  ovolicc2lem3  25870  volfiniun  25898  iundisj  25899  dvne0  26361  lhop2  26365  itgsubstlem  26398  coemullem  26599  rnplynfin  26660  plyexmo  26666  logccne0  26936  rtprmirr  27118  lgamgulmlem1  27386  wilthlem2  27426  wilth  27428  mumul  27538  chtublem  27568  perfect1  27585  lgsdilem2  27690  lgsne0  27692  lgsqrlem2  27704  lgseisenlem1  27732  lgseisenlem2  27733  lgsquadlem1  27737  lgsquadlem2  27738  lgsquadlem3  27739  lgsquad2lem1  27741  2sqblem  27788  chebbnd1lem1  27826  pntpbnd2  27944  pntlem3  27966  ostth  27996  flt4lem5elem  28011  flt4lem7  28019  nna4b4nsq  28020  ltsval2  28043  nolt02o  28082  nosupbnd1lem2  28096  nosupbnd1  28101  nosupbnd2  28103  noinfbnd1lem2  28111  noinfbnd1  28116  noinfbnd2  28118  noetasuplem4  28123  noetainflem4  28127  cutbdaybnd2lim  28213  oniso  28687  bdayfinbndlem1  28883  z12bdaylem1  28886  umgrnloop0  29717  usgrnloop0ALT  29816  wlkp1lem2  30283  pthdlem2lem  30383  chirredlem1  33022  iundisjf  33255  ofpreima2  33332  iundisjfi  33458  rprmndvdsru  34131  acwer1prc  35852  vonf1onprcf1ac  36044  onprcf1acwevd  36047  antnest  36621  antnestlaw3lem  36622  mirimanoffr  36627  fundmpss  36710  dfon2lem4  36726  dfon2lem7  36729  broutsideof2  37065  outsidele  37075  nn0prpwlem  37288  onint1  37415  fin2so  38722  lindsadd  38728  suceldisj  39942  lpssat  40262  exatleN  40653  3noncolr2  40698  4noncolr3  40702  3dimlem3  40710  3dimlem3OLDN  40711  3dimlem4a  40712  3dimlem4  40713  3dimlem4OLDN  40714  3atlem4  40735  3atlem5  40736  3atlem6  40737  llnnleat  40762  lplnnle2at  40790  lvolnle3at  40831  4atlem0a  40842  4atlem0ae  40843  dalem21  40943  dalem54  40975  cdlemblem  41042  lhpmcvr4N  41275  4atexlemnclw  41319  cdlemd3  41449  cdleme3g  41483  cdleme3h  41484  cdleme7aa  41491  cdleme7d  41495  cdleme7ga  41497  cdleme11c  41510  cdleme15b  41524  cdleme20zN  41550  cdleme21b  41575  cdleme21c  41576  cdleme21ct  41578  cdleme22b  41590  cdleme32b  41691  cdleme35fnpq  41698  cdleme35f  41703  cdleme36a  41709  cdleme42c  41721  cdleme48bw  41751  cdlemf1  41810  cdlemg2fv2  41849  cdlemg7fvbwN  41856  cdlemg4  41866  cdlemg6c  41869  cdlemg27a  41941  cdlemg27b  41945  cdlemk3  42082  dia2dimlem1  42313  dihord6apre  42505  dihord6b  42509  dihord5apre  42511  dihglbcpreN  42549  dihmeetlem6  42558  dochnel2  42641  dochexmidlem7  42715  lspindp5  43019  mapdh8b  43029  hdmapip0  43164  aks6d1c2p2  43361  pellexlem6  44034  elpell14qr2  44062  pellfundglb  44085  jm2.19  44193  jm2.26lem3  44201  setindtr  44224  harinf  44234  dgraa0p  44343  tfsconcatb0  44538  gneispace0nelrn3  45334  nellindf  51250