Theorem mtod 197

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 195	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  198  mtbid  323  mtbird  324  mtand  814  mtord  878  po2nr  5601  po3nr  5602  ordn2lp  6381  ordnbtwn  6454  fpropnf1  7262  tfi  7838  nnlim  7865  frrlem14  8280  smoord  8361  tz7.48-3  8440  oalimcl  8556  omlimcl  8574  oneo  8577  omopth2  8580  nnneo  8650  sucdom2OLD  9078  mapdom2  9144  sucdom2  9202  php2  9207  php3OLD  9220  onomeneqOLD  9225  1sdom2dom  9243  isfinite2  9297  domunfican  9316  ordtypelem7  9515  unxpwdom2  9579  cantnfp1lem2  9670  oemapvali  9675  cantnflem1  9680  cantnflem2  9681  rankpwi  9814  tskwe  9941  alephordi  10065  alephdom  10072  cardaleph  10080  cflim2  10254  isfin4p1  10306  fin23lem26  10316  fin1a2lem13  10403  axcclem  10448  fpwwe2lem11  10632  fpwwe2lem12  10633  fpwwe2  10634  pwxpndom2  10656  pwxpndom  10657  pwdjundom  10658  gchaleph  10662  r1wunlim  10728  inatsk  10769  tskuni  10774  gruina  10809  prlem934  11024  dedekind  11373  prodge0rd  13077  qextltlem  13177  ixxub  13341  ixxlb  13342  seqf1olem1  14003  facndiv  14244  cnpart  15183  rlimuni  15490  rlimcld2  15518  isercoll  15610  incexclem  15778  isumltss  15790  alzdvds  16259  fzm1ndvds  16261  fzo0dvdseq  16262  bitsfzolem  16371  smuval2  16419  smupvallem  16420  bezoutlem3  16479  rpdvds  16593  nonsq  16691  prmdiv  16714  odzdvds  16724  pcprendvds  16769  pcprendvds2  16770  pcpremul  16772  pcdvdsb  16798  pcadd2  16819  pockthlem  16834  prmreclem5  16849  prmreclem6  16850  1arith  16856  4sqlem11  16884  vdwlem11  16920  vdwlem12  16921  ramubcl  16947  mrissmrcd  17580  pltnlt  18289  acsfiindd  18502  odcl2  19427  gexnnod  19450  pgpssslw  19476  torsubg  19716  lt6abl  19757  ablfacrplem  19929  pgpfac1lem3  19941  ablsimpnosubgd  19968  irredrmul  20233  islbs3  20760  lbsextlem3  20765  lbsextlem4  20766  f1lindf  21368  mvrf1  21536  perfopn  22680  pnfnei  22715  mnfnei  22716  haust1  22847  cmpcld  22897  ptbasfi  23076  fbncp  23334  isfild  23353  fbasfip  23363  filufint  23415  rnelfmlem  23447  fmfnfm  23453  fclscf  23520  ptcmplem3  23549  opnsubg  23603  bldisj  23895  iccntr  24328  icccmplem2  24330  reconnlem1  24333  reconnlem2  24334  evth  24466  lebnumlem3  24470  ovolicc2lem3  25027  volfiniun  25055  iundisj  25056  dvne0  25519  lhop2  25523  itgsubstlem  25556  coemullem  25755  plyexmo  25817  logccne0  26078  lgamgulmlem1  26522  wilthlem2  26562  wilth  26564  mumul  26674  chtublem  26703  perfect1  26720  lgsdilem2  26825  lgsne0  26827  lgsqrlem2  26839  lgseisenlem1  26867  lgseisenlem2  26868  lgsquadlem1  26872  lgsquadlem2  26873  lgsquadlem3  26874  lgsquad2lem1  26876  2sqblem  26923  chebbnd1lem1  26961  pntpbnd2  27079  pntlem3  27101  ostth  27131  sltval2  27148  nolt02o  27187  nosupbnd1lem2  27201  nosupbnd1  27206  nosupbnd2  27208  noinfbnd1lem2  27216  noinfbnd1  27221  noinfbnd2  27223  noetasuplem4  27228  noetainflem4  27232  scutbdaybnd2lim  27307  umgrnloop0  28358  usgrnloop0ALT  28451  wlkp1lem2  28920  pthdlem2lem  29013  chirredlem1  31630  iundisjf  31807  ofpreima2  31878  iundisjfi  31994  fundmpss  34726  dfon2lem4  34746  dfon2lem7  34749  broutsideof2  35082  outsidele  35092  nn0prpwlem  35195  onint1  35322  fin2so  36463  lindsadd  36469  lpssat  37871  exatleN  38263  3noncolr2  38308  4noncolr3  38312  3dimlem3  38320  3dimlem3OLDN  38321  3dimlem4a  38322  3dimlem4  38323  3dimlem4OLDN  38324  3atlem4  38345  3atlem5  38346  3atlem6  38347  llnnleat  38372  lplnnle2at  38400  lvolnle3at  38441  4atlem0a  38452  4atlem0ae  38453  dalem21  38553  dalem54  38585  cdlemblem  38652  lhpmcvr4N  38885  4atexlemnclw  38929  cdlemd3  39059  cdleme3g  39093  cdleme3h  39094  cdleme7aa  39101  cdleme7d  39105  cdleme7ga  39107  cdleme11c  39120  cdleme15b  39134  cdleme20zN  39160  cdleme21b  39185  cdleme21c  39186  cdleme21ct  39188  cdleme22b  39200  cdleme32b  39301  cdleme35fnpq  39308  cdleme35f  39313  cdleme36a  39319  cdleme42c  39331  cdleme48bw  39361  cdlemf1  39420  cdlemg2fv2  39459  cdlemg7fvbwN  39466  cdlemg4  39476  cdlemg6c  39479  cdlemg27a  39551  cdlemg27b  39555  cdlemk3  39692  dia2dimlem1  39923  dihord6apre  40115  dihord6b  40119  dihord5apre  40121  dihglbcpreN  40159  dihmeetlem6  40168  dochnel2  40251  dochexmidlem7  40325  lspindp5  40629  mapdh8b  40639  hdmapip0  40774  aks6d1c2p2  40945  rtprmirr  41233  flt4lem5elem  41389  flt4lem7  41397  nna4b4nsq  41398  pellexlem6  41557  elpell14qr2  41585  pellfundglb  41608  jm2.19  41717  jm2.26lem3  41725  setindtr  41748  harinf  41758  dgraa0p  41876  tfsconcatb0  42079  gneispace0nelrn3  42878