Theorem mtod 199

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 197	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  200  mtbid  325  mtbird  326  mtand  821  mtord  885  po2nr  5547  po3nr  5548  ordn2lp  6337  ordnbtwn  6412  fpropnf1  7218  tfi  7800  nnlim  7827  frrlem14  8246  smoord  8302  tz7.48-3  8380  oalimcl  8492  omlimcl  8510  oneo  8513  omopth2  8516  nnneo  8588  mapdom2  9083  sucdom2  9134  php2  9139  1sdom2dom  9161  isfinite2  9205  domunfican  9229  ordtypelem7  9436  unxpwdom2  9500  cantnfp1lem2  9598  oemapvali  9603  cantnflem1  9608  cantnflem2  9609  rankpwi  9745  tskwe  9872  alephordi  9994  alephdom  10001  cardaleph  10009  cflim2  10183  isfin4p1  10235  fin23lem26  10245  fin1a2lem13  10332  axcclem  10377  fpwwe2lem11  10562  fpwwe2lem12  10563  fpwwe2  10564  pwxpndom2  10586  pwxpndom  10587  pwdjundom  10588  gchaleph  10592  r1wunlim  10658  inatsk  10699  tskuni  10704  gruina  10739  prlem934  10954  dedekind  11307  prodge0rd  13049  qextltlem  13152  ixxub  13317  ixxlb  13318  seqf1olem1  14001  facndiv  14248  cnpart  15200  rlimuni  15510  rlimcld2  15538  isercoll  15628  incexclem  15799  isumltss  15811  alzdvds  16287  fzm1ndvds  16289  fzo0dvdseq  16290  bitsfzolem  16401  smuval2  16449  smupvallem  16450  bezoutlem3  16508  rpdvds  16627  nonsq  16727  prmdiv  16753  odzdvds  16764  pcprendvds  16809  pcprendvds2  16810  pcpremul  16812  pcdvdsb  16838  pcadd2  16859  pockthlem  16874  prmreclem5  16889  prmreclem6  16890  1arith  16896  4sqlem11  16924  vdwlem11  16960  vdwlem12  16961  ramubcl  16987  mrissmrcd  17604  pltnlt  18302  acsfiindd  18517  odcl2  19538  gexnnod  19561  pgpssslw  19587  torsubg  19827  lt6abl  19868  ablfacrplem  20040  pgpfac1lem3  20052  ablsimpnosubgd  20079  irredrmul  20405  islbs3  21155  lbsextlem3  21160  lbsextlem4  21161  f1lindf  21804  mvrf1  21967  psdmul  22161  perfopn  23175  pnfnei  23210  mnfnei  23211  haust1  23342  cmpcld  23392  ptbasfi  23571  fbncp  23829  isfild  23848  fbasfip  23858  filufint  23910  rnelfmlem  23942  fmfnfm  23948  fclscf  24015  ptcmplem3  24044  opnsubg  24098  bldisj  24388  iccntr  24812  icccmplem2  24814  reconnlem1  24817  reconnlem2  24818  evth  24951  lebnumlem3  24955  ovolicc2lem3  25511  volfiniun  25539  iundisj  25540  dvne0  26003  lhop2  26007  itgsubstlem  26040  coemullem  26240  plyexmo  26304  logccne0  26567  rtprmirr  26749  lgamgulmlem1  27017  wilthlem2  27057  wilth  27059  mumul  27169  chtublem  27199  perfect1  27216  lgsdilem2  27321  lgsne0  27323  lgsqrlem2  27335  lgseisenlem1  27363  lgseisenlem2  27364  lgsquadlem1  27368  lgsquadlem2  27369  lgsquadlem3  27370  lgsquad2lem1  27372  2sqblem  27419  chebbnd1lem1  27457  pntpbnd2  27575  pntlem3  27597  ostth  27627  ltsval2  27645  nolt02o  27684  nosupbnd1lem2  27698  nosupbnd1  27703  nosupbnd2  27705  noinfbnd1lem2  27713  noinfbnd1  27718  noinfbnd2  27720  noetasuplem4  27725  noetainflem4  27729  cutbdaybnd2lim  27814  oniso  28288  bdayfinbndlem1  28484  z12bdaylem1  28487  umgrnloop0  29203  usgrnloop0ALT  29299  wlkp1lem2  29766  pthdlem2lem  29860  chirredlem1  32486  iundisjf  32685  ofpreima2  32765  iundisjfi  32895  rprmndvdsru  33619  antnest  35924  antnestlaw3lem  35925  fundmpss  36002  dfon2lem4  36019  dfon2lem7  36022  broutsideof2  36357  outsidele  36367  nn0prpwlem  36557  onint1  36684  fin2so  37981  lindsadd  37987  suceldisj  39192  lpssat  39512  exatleN  39903  3noncolr2  39948  4noncolr3  39952  3dimlem3  39960  3dimlem3OLDN  39961  3dimlem4a  39962  3dimlem4  39963  3dimlem4OLDN  39964  3atlem4  39985  3atlem5  39986  3atlem6  39987  llnnleat  40012  lplnnle2at  40040  lvolnle3at  40081  4atlem0a  40092  4atlem0ae  40093  dalem21  40193  dalem54  40225  cdlemblem  40292  lhpmcvr4N  40525  4atexlemnclw  40569  cdlemd3  40699  cdleme3g  40733  cdleme3h  40734  cdleme7aa  40741  cdleme7d  40745  cdleme7ga  40747  cdleme11c  40760  cdleme15b  40774  cdleme20zN  40800  cdleme21b  40825  cdleme21c  40826  cdleme21ct  40828  cdleme22b  40840  cdleme32b  40941  cdleme35fnpq  40948  cdleme35f  40953  cdleme36a  40959  cdleme42c  40971  cdleme48bw  41001  cdlemf1  41060  cdlemg2fv2  41099  cdlemg7fvbwN  41106  cdlemg4  41116  cdlemg6c  41119  cdlemg27a  41191  cdlemg27b  41195  cdlemk3  41332  dia2dimlem1  41563  dihord6apre  41755  dihord6b  41759  dihord5apre  41761  dihglbcpreN  41799  dihmeetlem6  41808  dochnel2  41891  dochexmidlem7  41965  lspindp5  42269  mapdh8b  42279  hdmapip0  42414  aks6d1c2p2  42611  flt4lem5elem  43108  flt4lem7  43116  nna4b4nsq  43117  pellexlem6  43286  elpell14qr2  43314  pellfundglb  43337  jm2.19  43445  jm2.26lem3  43453  setindtr  43476  harinf  43486  dgraa0p  43601  tfsconcatb0  43796  gneispace0nelrn3  44593