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  nrmod  3846  po2nr  5585  po3nr  5586  ordn2lp  6382  ordnbtwn  6458  fpropnf1  7267  tfi  7850  nnlim  7877  frrlem14  8297  smoord  8353  tz7.48-3  8432  oalimcl  8546  omlimcl  8564  oneo  8567  omopth2  8570  nnneo  8642  mapdom2  9137  sucdom2  9188  php2  9193  1sdom2dom  9215  isfinite2  9259  domunfican  9282  ordtypelem7  9487  unxpwdom2  9551  cantnfp1lem2  9649  oemapvali  9654  cantnflem1  9659  cantnflem2  9660  rankpwi  9796  tskwe  9937  alephordi  10059  alephdom  10066  cardaleph  10074  cflim2  10248  isfin4p1  10300  fin23lem26  10310  fin1a2lem13  10397  axcclem  10442  fpwwe2lem11  10627  fpwwe2lem12  10628  fpwwe2  10629  pwxpndom2  10651  pwxpndom  10652  pwdjundom  10653  gchaleph  10657  r1wunlim  10723  inatsk  10764  tskuni  10769  gruina  10804  prlem934  11019  dedekind  11374  prodge0rd  13126  qextltlem  13229  ixxub  13394  ixxlb  13395  seqf1olem1  14079  facndiv  14326  cnpart  15293  rlimuni  15603  rlimcld2  15631  isercoll  15721  incexclem  15892  isumltss  15904  alzdvds  16379  fzm1ndvds  16381  fzo0dvdseq  16382  bitsfzolem  16493  smuval2  16541  smupvallem  16542  bezoutlem3  16600  rpdvds  16719  nonsq  16819  prmdiv  16845  odzdvds  16856  pcprendvds  16901  pcprendvds2  16902  pcpremul  16904  pcdvdsb  16930  pcadd2  16951  pockthlem  16966  prmreclem5  16981  prmreclem6  16982  1arith  16988  4sqlem11  17016  vdwlem11  17052  vdwlem12  17053  ramubcl  17079  mrissmrcd  17697  pltnlt  18395  acsfiindd  18610  odcl2  19636  gexnnod  19659  pgpssslw  19685  torsubg  19925  lt6abl  19966  ablfacrplem  20138  pgpfac1lem3  20150  ablsimpnosubgd  20177  irredrmul  20510  islbs3  21260  lbsextlem3  21265  lbsextlem4  21266  f1lindf  21953  mvrf1  22116  psdmul  22310  perfopn  23323  pnfnei  23358  mnfnei  23359  haust1  23490  cmpcld  23540  ptbasfi  23719  fbncp  23977  isfild  23996  fbasfip  24006  filufint  24058  rnelfmlem  24090  fmfnfm  24096  fclscf  24163  ptcmplem3  24192  opnsubg  24246  bldisj  24536  iccntr  24960  icccmplem2  24962  reconnlem1  24965  reconnlem2  24966  evth  25099  lebnumlem3  25103  ovolicc2lem3  25659  volfiniun  25687  iundisj  25688  dvne0  26151  lhop2  26155  itgsubstlem  26188  coemullem  26388  plyexmo  26455  logccne0  26721  rtprmirr  26903  lgamgulmlem1  27171  wilthlem2  27211  wilth  27213  mumul  27323  chtublem  27353  perfect1  27370  lgsdilem2  27475  lgsne0  27477  lgsqrlem2  27489  lgseisenlem1  27517  lgseisenlem2  27518  lgsquadlem1  27522  lgsquadlem2  27523  lgsquadlem3  27524  lgsquad2lem1  27526  2sqblem  27573  chebbnd1lem1  27611  pntpbnd2  27729  pntlem3  27751  ostth  27781  ltsval2  27798  nolt02o  27837  nosupbnd1lem2  27851  nosupbnd1  27856  nosupbnd2  27858  noinfbnd1lem2  27866  noinfbnd1  27871  noinfbnd2  27873  noetasuplem4  27878  noetainflem4  27882  cutbdaybnd2lim  27968  oniso  28442  bdayfinbndlem1  28638  z12bdaylem1  28641  umgrnloop0  29437  usgrnloop0ALT  29533  wlkp1lem2  30000  pthdlem2lem  30094  chirredlem1  32720  iundisjf  32912  ofpreima2  32989  iundisjfi  33119  rprmndvdsru  33797  antnest  36159  antnestlaw3lem  36160  fundmpss  36237  dfon2lem4  36254  dfon2lem7  36257  broutsideof2  36592  outsidele  36602  nn0prpwlem  36811  onint1  36938  fin2so  38236  lindsadd  38242  suceldisj  39445  lpssat  39765  exatleN  40156  3noncolr2  40201  4noncolr3  40205  3dimlem3  40213  3dimlem3OLDN  40214  3dimlem4a  40215  3dimlem4  40216  3dimlem4OLDN  40217  3atlem4  40238  3atlem5  40239  3atlem6  40240  llnnleat  40265  lplnnle2at  40293  lvolnle3at  40334  4atlem0a  40345  4atlem0ae  40346  dalem21  40446  dalem54  40478  cdlemblem  40545  lhpmcvr4N  40778  4atexlemnclw  40822  cdlemd3  40952  cdleme3g  40986  cdleme3h  40987  cdleme7aa  40994  cdleme7d  40998  cdleme7ga  41000  cdleme11c  41013  cdleme15b  41027  cdleme20zN  41053  cdleme21b  41078  cdleme21c  41079  cdleme21ct  41081  cdleme22b  41093  cdleme32b  41194  cdleme35fnpq  41201  cdleme35f  41206  cdleme36a  41212  cdleme42c  41224  cdleme48bw  41254  cdlemf1  41313  cdlemg2fv2  41352  cdlemg7fvbwN  41359  cdlemg4  41369  cdlemg6c  41372  cdlemg27a  41444  cdlemg27b  41448  cdlemk3  41585  dia2dimlem1  41816  dihord6apre  42008  dihord6b  42012  dihord5apre  42014  dihglbcpreN  42052  dihmeetlem6  42061  dochnel2  42144  dochexmidlem7  42218  lspindp5  42522  mapdh8b  42532  hdmapip0  42667  aks6d1c2p2  42864  flt4lem5elem  43363  flt4lem7  43371  nna4b4nsq  43372  pellexlem6  43541  elpell14qr2  43569  pellfundglb  43592  jm2.19  43700  jm2.26lem3  43708  setindtr  43731  harinf  43741  dgraa0p  43856  tfsconcatb0  44051  gneispace0nelrn3  44848