Theorem mtod 198

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 196	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  199  mtbid  324  mtbird  325  mtand  815  mtord  879  po2nr  5575  po3nr  5576  ordn2lp  6372  ordnbtwn  6446  fpropnf1  7259  tfi  7846  nnlim  7873  frrlem14  8296  smoord  8377  tz7.48-3  8456  oalimcl  8570  omlimcl  8588  oneo  8591  omopth2  8594  nnneo  8665  sucdom2OLD  9094  mapdom2  9160  sucdom2  9215  php2  9220  php3OLD  9231  onomeneqOLD  9236  1sdom2dom  9253  isfinite2  9304  domunfican  9331  ordtypelem7  9536  unxpwdom2  9600  cantnfp1lem2  9691  oemapvali  9696  cantnflem1  9701  cantnflem2  9702  rankpwi  9835  tskwe  9962  alephordi  10086  alephdom  10093  cardaleph  10101  cflim2  10275  isfin4p1  10327  fin23lem26  10337  fin1a2lem13  10424  axcclem  10469  fpwwe2lem11  10653  fpwwe2lem12  10654  fpwwe2  10655  pwxpndom2  10677  pwxpndom  10678  pwdjundom  10679  gchaleph  10683  r1wunlim  10749  inatsk  10790  tskuni  10795  gruina  10830  prlem934  11045  dedekind  11396  prodge0rd  13114  qextltlem  13216  ixxub  13381  ixxlb  13382  seqf1olem1  14057  facndiv  14304  cnpart  15257  rlimuni  15564  rlimcld2  15592  isercoll  15682  incexclem  15850  isumltss  15862  alzdvds  16337  fzm1ndvds  16339  fzo0dvdseq  16340  bitsfzolem  16451  smuval2  16499  smupvallem  16500  bezoutlem3  16558  rpdvds  16677  nonsq  16776  prmdiv  16802  odzdvds  16813  pcprendvds  16858  pcprendvds2  16859  pcpremul  16861  pcdvdsb  16887  pcadd2  16908  pockthlem  16923  prmreclem5  16938  prmreclem6  16939  1arith  16945  4sqlem11  16973  vdwlem11  17009  vdwlem12  17010  ramubcl  17036  mrissmrcd  17650  pltnlt  18348  acsfiindd  18561  odcl2  19544  gexnnod  19567  pgpssslw  19593  torsubg  19833  lt6abl  19874  ablfacrplem  20046  pgpfac1lem3  20058  ablsimpnosubgd  20085  irredrmul  20385  islbs3  21114  lbsextlem3  21119  lbsextlem4  21120  f1lindf  21780  mvrf1  21944  psdmul  22102  perfopn  23121  pnfnei  23156  mnfnei  23157  haust1  23288  cmpcld  23338  ptbasfi  23517  fbncp  23775  isfild  23794  fbasfip  23804  filufint  23856  rnelfmlem  23888  fmfnfm  23894  fclscf  23961  ptcmplem3  23990  opnsubg  24044  bldisj  24335  iccntr  24759  icccmplem2  24761  reconnlem1  24764  reconnlem2  24765  evth  24907  lebnumlem3  24911  ovolicc2lem3  25470  volfiniun  25498  iundisj  25499  dvne0  25966  lhop2  25970  itgsubstlem  26005  coemullem  26205  plyexmo  26271  logccne0  26537  rtprmirr  26720  lgamgulmlem1  26989  wilthlem2  27029  wilth  27031  mumul  27141  chtublem  27172  perfect1  27189  lgsdilem2  27294  lgsne0  27296  lgsqrlem2  27308  lgseisenlem1  27336  lgseisenlem2  27337  lgsquadlem1  27341  lgsquadlem2  27342  lgsquadlem3  27343  lgsquad2lem1  27345  2sqblem  27392  chebbnd1lem1  27430  pntpbnd2  27548  pntlem3  27570  ostth  27600  sltval2  27618  nolt02o  27657  nosupbnd1lem2  27671  nosupbnd1  27676  nosupbnd2  27678  noinfbnd1lem2  27686  noinfbnd1  27691  noinfbnd2  27693  noetasuplem4  27698  noetainflem4  27702  scutbdaybnd2lim  27779  umgrnloop0  29034  usgrnloop0ALT  29130  wlkp1lem2  29600  pthdlem2lem  29695  chirredlem1  32317  iundisjf  32516  ofpreima2  32590  iundisjfi  32719  rprmndvdsru  33490  antnest  35657  fundmpss  35730  dfon2lem4  35750  dfon2lem7  35753  broutsideof2  36086  outsidele  36096  nn0prpwlem  36286  onint1  36413  fin2so  37577  lindsadd  37583  lpssat  38977  exatleN  39369  3noncolr2  39414  4noncolr3  39418  3dimlem3  39426  3dimlem3OLDN  39427  3dimlem4a  39428  3dimlem4  39429  3dimlem4OLDN  39430  3atlem4  39451  3atlem5  39452  3atlem6  39453  llnnleat  39478  lplnnle2at  39506  lvolnle3at  39547  4atlem0a  39558  4atlem0ae  39559  dalem21  39659  dalem54  39691  cdlemblem  39758  lhpmcvr4N  39991  4atexlemnclw  40035  cdlemd3  40165  cdleme3g  40199  cdleme3h  40200  cdleme7aa  40207  cdleme7d  40211  cdleme7ga  40213  cdleme11c  40226  cdleme15b  40240  cdleme20zN  40266  cdleme21b  40291  cdleme21c  40292  cdleme21ct  40294  cdleme22b  40306  cdleme32b  40407  cdleme35fnpq  40414  cdleme35f  40419  cdleme36a  40425  cdleme42c  40437  cdleme48bw  40467  cdlemf1  40526  cdlemg2fv2  40565  cdlemg7fvbwN  40572  cdlemg4  40582  cdlemg6c  40585  cdlemg27a  40657  cdlemg27b  40661  cdlemk3  40798  dia2dimlem1  41029  dihord6apre  41221  dihord6b  41225  dihord5apre  41227  dihglbcpreN  41265  dihmeetlem6  41274  dochnel2  41357  dochexmidlem7  41431  lspindp5  41735  mapdh8b  41745  hdmapip0  41880  aks6d1c2p2  42078  flt4lem5elem  42621  flt4lem7  42629  nna4b4nsq  42630  pellexlem6  42804  elpell14qr2  42832  pellfundglb  42855  jm2.19  42964  jm2.26lem3  42972  setindtr  42995  harinf  43005  dgraa0p  43120  tfsconcatb0  43315  gneispace0nelrn3  44113