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  816  mtord  880  po2nr  5546  po3nr  5547  ordn2lp  6337  ordnbtwn  6412  fpropnf1  7215  tfi  7797  nnlim  7824  frrlem14  8242  smoord  8298  tz7.48-3  8376  oalimcl  8488  omlimcl  8506  oneo  8509  omopth2  8512  nnneo  8584  mapdom2  9079  sucdom2  9130  php2  9135  1sdom2dom  9157  isfinite2  9201  domunfican  9225  ordtypelem7  9432  unxpwdom2  9496  cantnfp1lem2  9591  oemapvali  9596  cantnflem1  9601  cantnflem2  9602  rankpwi  9738  tskwe  9865  alephordi  9987  alephdom  9994  cardaleph  10002  cflim2  10176  isfin4p1  10228  fin23lem26  10238  fin1a2lem13  10325  axcclem  10370  fpwwe2lem11  10555  fpwwe2lem12  10556  fpwwe2  10557  pwxpndom2  10579  pwxpndom  10580  pwdjundom  10581  gchaleph  10585  r1wunlim  10651  inatsk  10692  tskuni  10697  gruina  10732  prlem934  10947  dedekind  11300  prodge0rd  13042  qextltlem  13145  ixxub  13310  ixxlb  13311  seqf1olem1  13994  facndiv  14241  cnpart  15193  rlimuni  15503  rlimcld2  15531  isercoll  15621  incexclem  15792  isumltss  15804  alzdvds  16280  fzm1ndvds  16282  fzo0dvdseq  16283  bitsfzolem  16394  smuval2  16442  smupvallem  16443  bezoutlem3  16501  rpdvds  16620  nonsq  16720  prmdiv  16746  odzdvds  16757  pcprendvds  16802  pcprendvds2  16803  pcpremul  16805  pcdvdsb  16831  pcadd2  16852  pockthlem  16867  prmreclem5  16882  prmreclem6  16883  1arith  16889  4sqlem11  16917  vdwlem11  16953  vdwlem12  16954  ramubcl  16980  mrissmrcd  17597  pltnlt  18295  acsfiindd  18510  odcl2  19531  gexnnod  19554  pgpssslw  19580  torsubg  19820  lt6abl  19861  ablfacrplem  20033  pgpfac1lem3  20045  ablsimpnosubgd  20072  irredrmul  20398  islbs3  21145  lbsextlem3  21150  lbsextlem4  21151  f1lindf  21812  mvrf1  21974  psdmul  22142  perfopn  23160  pnfnei  23195  mnfnei  23196  haust1  23327  cmpcld  23377  ptbasfi  23556  fbncp  23814  isfild  23833  fbasfip  23843  filufint  23895  rnelfmlem  23927  fmfnfm  23933  fclscf  24000  ptcmplem3  24029  opnsubg  24083  bldisj  24373  iccntr  24797  icccmplem2  24799  reconnlem1  24802  reconnlem2  24803  evth  24936  lebnumlem3  24940  ovolicc2lem3  25496  volfiniun  25524  iundisj  25525  dvne0  25988  lhop2  25992  itgsubstlem  26025  coemullem  26225  plyexmo  26290  logccne0  26555  rtprmirr  26737  lgamgulmlem1  27006  wilthlem2  27046  wilth  27048  mumul  27158  chtublem  27188  perfect1  27205  lgsdilem2  27310  lgsne0  27312  lgsqrlem2  27324  lgseisenlem1  27352  lgseisenlem2  27353  lgsquadlem1  27357  lgsquadlem2  27358  lgsquadlem3  27359  lgsquad2lem1  27361  2sqblem  27408  chebbnd1lem1  27446  pntpbnd2  27564  pntlem3  27586  ostth  27616  ltsval2  27634  nolt02o  27673  nosupbnd1lem2  27687  nosupbnd1  27692  nosupbnd2  27694  noinfbnd1lem2  27702  noinfbnd1  27707  noinfbnd2  27709  noetasuplem4  27714  noetainflem4  27718  cutbdaybnd2lim  27803  oniso  28277  bdayfinbndlem1  28473  z12bdaylem1  28476  umgrnloop0  29192  usgrnloop0ALT  29288  wlkp1lem2  29756  pthdlem2lem  29850  chirredlem1  32476  iundisjf  32674  ofpreima2  32754  iundisjfi  32884  rprmndvdsru  33604  antnest  35887  antnestlaw3lem  35888  fundmpss  35965  dfon2lem4  35982  dfon2lem7  35985  broutsideof2  36320  outsidele  36330  nn0prpwlem  36520  onint1  36647  fin2so  37942  lindsadd  37948  suceldisj  39153  lpssat  39473  exatleN  39864  3noncolr2  39909  4noncolr3  39913  3dimlem3  39921  3dimlem3OLDN  39922  3dimlem4a  39923  3dimlem4  39924  3dimlem4OLDN  39925  3atlem4  39946  3atlem5  39947  3atlem6  39948  llnnleat  39973  lplnnle2at  40001  lvolnle3at  40042  4atlem0a  40053  4atlem0ae  40054  dalem21  40154  dalem54  40186  cdlemblem  40253  lhpmcvr4N  40486  4atexlemnclw  40530  cdlemd3  40660  cdleme3g  40694  cdleme3h  40695  cdleme7aa  40702  cdleme7d  40706  cdleme7ga  40708  cdleme11c  40721  cdleme15b  40735  cdleme20zN  40761  cdleme21b  40786  cdleme21c  40787  cdleme21ct  40789  cdleme22b  40801  cdleme32b  40902  cdleme35fnpq  40909  cdleme35f  40914  cdleme36a  40920  cdleme42c  40932  cdleme48bw  40962  cdlemf1  41021  cdlemg2fv2  41060  cdlemg7fvbwN  41067  cdlemg4  41077  cdlemg6c  41080  cdlemg27a  41152  cdlemg27b  41156  cdlemk3  41293  dia2dimlem1  41524  dihord6apre  41716  dihord6b  41720  dihord5apre  41722  dihglbcpreN  41760  dihmeetlem6  41769  dochnel2  41852  dochexmidlem7  41926  lspindp5  42230  mapdh8b  42240  hdmapip0  42375  aks6d1c2p2  42572  flt4lem5elem  43098  flt4lem7  43106  nna4b4nsq  43107  pellexlem6  43280  elpell14qr2  43308  pellfundglb  43331  jm2.19  43439  jm2.26lem3  43447  setindtr  43470  harinf  43480  dgraa0p  43595  tfsconcatb0  43790  gneispace0nelrn3  44587