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  5538  po3nr  5539  ordn2lp  6326  ordnbtwn  6401  fpropnf1  7201  tfi  7783  nnlim  7810  frrlem14  8229  smoord  8285  tz7.48-3  8363  oalimcl  8475  omlimcl  8493  oneo  8496  omopth2  8499  nnneo  8570  mapdom2  9061  sucdom2  9112  php2  9117  1sdom2dom  9138  isfinite2  9182  domunfican  9206  ordtypelem7  9410  unxpwdom2  9474  cantnfp1lem2  9569  oemapvali  9574  cantnflem1  9579  cantnflem2  9580  rankpwi  9713  tskwe  9840  alephordi  9962  alephdom  9969  cardaleph  9977  cflim2  10151  isfin4p1  10203  fin23lem26  10213  fin1a2lem13  10300  axcclem  10345  fpwwe2lem11  10529  fpwwe2lem12  10530  fpwwe2  10531  pwxpndom2  10553  pwxpndom  10554  pwdjundom  10555  gchaleph  10559  r1wunlim  10625  inatsk  10666  tskuni  10671  gruina  10706  prlem934  10921  dedekind  11273  prodge0rd  12996  qextltlem  13098  ixxub  13263  ixxlb  13264  seqf1olem1  13945  facndiv  14192  cnpart  15144  rlimuni  15454  rlimcld2  15482  isercoll  15572  incexclem  15740  isumltss  15752  alzdvds  16228  fzm1ndvds  16230  fzo0dvdseq  16231  bitsfzolem  16342  smuval2  16390  smupvallem  16391  bezoutlem3  16449  rpdvds  16568  nonsq  16667  prmdiv  16693  odzdvds  16704  pcprendvds  16749  pcprendvds2  16750  pcpremul  16752  pcdvdsb  16778  pcadd2  16799  pockthlem  16814  prmreclem5  16829  prmreclem6  16830  1arith  16836  4sqlem11  16864  vdwlem11  16900  vdwlem12  16901  ramubcl  16927  mrissmrcd  17543  pltnlt  18241  acsfiindd  18456  odcl2  19475  gexnnod  19498  pgpssslw  19524  torsubg  19764  lt6abl  19805  ablfacrplem  19977  pgpfac1lem3  19989  ablsimpnosubgd  20016  irredrmul  20343  islbs3  21090  lbsextlem3  21095  lbsextlem4  21096  f1lindf  21757  mvrf1  21921  psdmul  22079  perfopn  23098  pnfnei  23133  mnfnei  23134  haust1  23265  cmpcld  23315  ptbasfi  23494  fbncp  23752  isfild  23771  fbasfip  23781  filufint  23833  rnelfmlem  23865  fmfnfm  23871  fclscf  23938  ptcmplem3  23967  opnsubg  24021  bldisj  24311  iccntr  24735  icccmplem2  24737  reconnlem1  24740  reconnlem2  24741  evth  24883  lebnumlem3  24887  ovolicc2lem3  25445  volfiniun  25473  iundisj  25474  dvne0  25941  lhop2  25945  itgsubstlem  25980  coemullem  26180  plyexmo  26246  logccne0  26512  rtprmirr  26695  lgamgulmlem1  26964  wilthlem2  27004  wilth  27006  mumul  27116  chtublem  27147  perfect1  27164  lgsdilem2  27269  lgsne0  27271  lgsqrlem2  27283  lgseisenlem1  27311  lgseisenlem2  27312  lgsquadlem1  27316  lgsquadlem2  27317  lgsquadlem3  27318  lgsquad2lem1  27320  2sqblem  27367  chebbnd1lem1  27405  pntpbnd2  27523  pntlem3  27545  ostth  27575  sltval2  27593  nolt02o  27632  nosupbnd1lem2  27646  nosupbnd1  27651  nosupbnd2  27653  noinfbnd1lem2  27661  noinfbnd1  27666  noinfbnd2  27668  noetasuplem4  27673  noetainflem4  27677  scutbdaybnd2lim  27756  onsiso  28203  umgrnloop0  29085  usgrnloop0ALT  29181  wlkp1lem2  29649  pthdlem2lem  29743  chirredlem1  32365  iundisjf  32564  ofpreima2  32643  iundisjfi  32773  rprmndvdsru  33489  antnest  35721  antnestlaw3lem  35722  fundmpss  35799  dfon2lem4  35819  dfon2lem7  35822  broutsideof2  36155  outsidele  36165  nn0prpwlem  36355  onint1  36482  fin2so  37646  lindsadd  37652  lpssat  39051  exatleN  39442  3noncolr2  39487  4noncolr3  39491  3dimlem3  39499  3dimlem3OLDN  39500  3dimlem4a  39501  3dimlem4  39502  3dimlem4OLDN  39503  3atlem4  39524  3atlem5  39525  3atlem6  39526  llnnleat  39551  lplnnle2at  39579  lvolnle3at  39620  4atlem0a  39631  4atlem0ae  39632  dalem21  39732  dalem54  39764  cdlemblem  39831  lhpmcvr4N  40064  4atexlemnclw  40108  cdlemd3  40238  cdleme3g  40272  cdleme3h  40273  cdleme7aa  40280  cdleme7d  40284  cdleme7ga  40286  cdleme11c  40299  cdleme15b  40313  cdleme20zN  40339  cdleme21b  40364  cdleme21c  40365  cdleme21ct  40367  cdleme22b  40379  cdleme32b  40480  cdleme35fnpq  40487  cdleme35f  40492  cdleme36a  40498  cdleme42c  40510  cdleme48bw  40540  cdlemf1  40599  cdlemg2fv2  40638  cdlemg7fvbwN  40645  cdlemg4  40655  cdlemg6c  40658  cdlemg27a  40730  cdlemg27b  40734  cdlemk3  40871  dia2dimlem1  41102  dihord6apre  41294  dihord6b  41298  dihord5apre  41300  dihglbcpreN  41338  dihmeetlem6  41347  dochnel2  41430  dochexmidlem7  41504  lspindp5  41808  mapdh8b  41818  hdmapip0  41953  aks6d1c2p2  42151  flt4lem5elem  42683  flt4lem7  42691  nna4b4nsq  42692  pellexlem6  42866  elpell14qr2  42894  pellfundglb  42917  jm2.19  43025  jm2.26lem3  43033  setindtr  43056  harinf  43066  dgraa0p  43181  tfsconcatb0  43376  gneispace0nelrn3  44174