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  5560  po3nr  5561  ordn2lp  6352  ordnbtwn  6427  fpropnf1  7242  tfi  7829  nnlim  7856  frrlem14  8278  smoord  8334  tz7.48-3  8412  oalimcl  8524  omlimcl  8542  oneo  8545  omopth2  8548  nnneo  8619  mapdom2  9112  sucdom2  9167  php2  9172  1sdom2dom  9194  isfinite2  9245  domunfican  9272  ordtypelem7  9477  unxpwdom2  9541  cantnfp1lem2  9632  oemapvali  9637  cantnflem1  9642  cantnflem2  9643  rankpwi  9776  tskwe  9903  alephordi  10027  alephdom  10034  cardaleph  10042  cflim2  10216  isfin4p1  10268  fin23lem26  10278  fin1a2lem13  10365  axcclem  10410  fpwwe2lem11  10594  fpwwe2lem12  10595  fpwwe2  10596  pwxpndom2  10618  pwxpndom  10619  pwdjundom  10620  gchaleph  10624  r1wunlim  10690  inatsk  10731  tskuni  10736  gruina  10771  prlem934  10986  dedekind  11337  prodge0rd  13060  qextltlem  13162  ixxub  13327  ixxlb  13328  seqf1olem1  14006  facndiv  14253  cnpart  15206  rlimuni  15516  rlimcld2  15544  isercoll  15634  incexclem  15802  isumltss  15814  alzdvds  16290  fzm1ndvds  16292  fzo0dvdseq  16293  bitsfzolem  16404  smuval2  16452  smupvallem  16453  bezoutlem3  16511  rpdvds  16630  nonsq  16729  prmdiv  16755  odzdvds  16766  pcprendvds  16811  pcprendvds2  16812  pcpremul  16814  pcdvdsb  16840  pcadd2  16861  pockthlem  16876  prmreclem5  16891  prmreclem6  16892  1arith  16898  4sqlem11  16926  vdwlem11  16962  vdwlem12  16963  ramubcl  16989  mrissmrcd  17601  pltnlt  18299  acsfiindd  18512  odcl2  19495  gexnnod  19518  pgpssslw  19544  torsubg  19784  lt6abl  19825  ablfacrplem  19997  pgpfac1lem3  20009  ablsimpnosubgd  20036  irredrmul  20336  islbs3  21065  lbsextlem3  21070  lbsextlem4  21071  f1lindf  21731  mvrf1  21895  psdmul  22053  perfopn  23072  pnfnei  23107  mnfnei  23108  haust1  23239  cmpcld  23289  ptbasfi  23468  fbncp  23726  isfild  23745  fbasfip  23755  filufint  23807  rnelfmlem  23839  fmfnfm  23845  fclscf  23912  ptcmplem3  23941  opnsubg  23995  bldisj  24286  iccntr  24710  icccmplem2  24712  reconnlem1  24715  reconnlem2  24716  evth  24858  lebnumlem3  24862  ovolicc2lem3  25420  volfiniun  25448  iundisj  25449  dvne0  25916  lhop2  25920  itgsubstlem  25955  coemullem  26155  plyexmo  26221  logccne0  26487  rtprmirr  26670  lgamgulmlem1  26939  wilthlem2  26979  wilth  26981  mumul  27091  chtublem  27122  perfect1  27139  lgsdilem2  27244  lgsne0  27246  lgsqrlem2  27258  lgseisenlem1  27286  lgseisenlem2  27287  lgsquadlem1  27291  lgsquadlem2  27292  lgsquadlem3  27293  lgsquad2lem1  27295  2sqblem  27342  chebbnd1lem1  27380  pntpbnd2  27498  pntlem3  27520  ostth  27550  sltval2  27568  nolt02o  27607  nosupbnd1lem2  27621  nosupbnd1  27626  nosupbnd2  27628  noinfbnd1lem2  27636  noinfbnd1  27641  noinfbnd2  27643  noetasuplem4  27648  noetainflem4  27652  scutbdaybnd2lim  27729  onsiso  28169  umgrnloop0  29036  usgrnloop0ALT  29132  wlkp1lem2  29602  pthdlem2lem  29697  chirredlem1  32319  iundisjf  32518  ofpreima2  32590  iundisjfi  32719  rprmndvdsru  33500  antnest  35676  antnestlaw3lem  35677  fundmpss  35754  dfon2lem4  35774  dfon2lem7  35777  broutsideof2  36110  outsidele  36120  nn0prpwlem  36310  onint1  36437  fin2so  37601  lindsadd  37607  lpssat  39006  exatleN  39398  3noncolr2  39443  4noncolr3  39447  3dimlem3  39455  3dimlem3OLDN  39456  3dimlem4a  39457  3dimlem4  39458  3dimlem4OLDN  39459  3atlem4  39480  3atlem5  39481  3atlem6  39482  llnnleat  39507  lplnnle2at  39535  lvolnle3at  39576  4atlem0a  39587  4atlem0ae  39588  dalem21  39688  dalem54  39720  cdlemblem  39787  lhpmcvr4N  40020  4atexlemnclw  40064  cdlemd3  40194  cdleme3g  40228  cdleme3h  40229  cdleme7aa  40236  cdleme7d  40240  cdleme7ga  40242  cdleme11c  40255  cdleme15b  40269  cdleme20zN  40295  cdleme21b  40320  cdleme21c  40321  cdleme21ct  40323  cdleme22b  40335  cdleme32b  40436  cdleme35fnpq  40443  cdleme35f  40448  cdleme36a  40454  cdleme42c  40466  cdleme48bw  40496  cdlemf1  40555  cdlemg2fv2  40594  cdlemg7fvbwN  40601  cdlemg4  40611  cdlemg6c  40614  cdlemg27a  40686  cdlemg27b  40690  cdlemk3  40827  dia2dimlem1  41058  dihord6apre  41250  dihord6b  41254  dihord5apre  41256  dihglbcpreN  41294  dihmeetlem6  41303  dochnel2  41386  dochexmidlem7  41460  lspindp5  41764  mapdh8b  41774  hdmapip0  41909  aks6d1c2p2  42107  flt4lem5elem  42639  flt4lem7  42647  nna4b4nsq  42648  pellexlem6  42822  elpell14qr2  42850  pellfundglb  42873  jm2.19  42982  jm2.26lem3  42990  setindtr  43013  harinf  43023  dgraa0p  43138  tfsconcatb0  43333  gneispace0nelrn3  44131