Theorem mtod 188

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 186	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  189  mtbid  313  mtbird  314  mtand  689  mtord  690  po2nr  4972  po3nr  4973  ordn2lp  5660  ordnbtwn  5733  tfi  6945  nnlim  6970  smoord  7349  tz7.48-3  7426  oalimcl  7527  omlimcl  7545  oneo  7548  omopth2  7551  nnneo  7618  mapdom2  8016  php3  8031  onomeneq  8035  sucdom2  8041  isfinite2  8103  domunfican  8118  ordtypelem7  8312  unxpwdom2  8376  cantnfp1lem2  8459  oemapvali  8464  cantnflem1  8469  cantnflem2  8470  rankpwi  8569  tskwe  8659  alephordi  8780  alephdom  8787  cardaleph  8795  cflim2  8968  isfin4-3  9020  fin23lem26  9030  fin1a2lem13  9117  axcclem  9162  fpwwe2lem12  9342  fpwwe2lem13  9343  fpwwe2  9344  pwxpndom2  9366  pwxpndom  9367  pwcdandom  9368  gchaleph  9372  r1wunlim  9438  inatsk  9479  tskuni  9484  gruina  9519  prlem934  9734  dedekind  10079  qextltlem  11907  ixxub  12067  ixxlb  12068  seqf1olem1  12702  facndiv  12937  cnpart  13828  rlimuni  14129  rlimcld2  14157  isercoll  14246  incexclem  14407  isumltss  14419  alzdvds  14880  fzm1ndvds  14882  fzo0dvdseq  14883  bitsfzolem  14994  smuval2  15042  smupvallem  15043  bezoutlem3  15096  rpdvds  15212  nonsq  15305  prmdiv  15328  odzdvds  15338  pcprendvds  15383  pcprendvds2  15384  pcpremul  15386  pcdvdsb  15411  pcadd2  15432  pockthlem  15447  prmreclem5  15462  prmreclem6  15463  1arith  15469  4sqlem11  15497  vdwlem11  15533  vdwlem12  15534  ramubcl  15560  mrissmrcd  16123  pltnlt  16791  acsfiindd  17000  odcl2  17805  gexnnod  17826  pgpssslw  17852  torsubg  18080  lt6abl  18119  ablfacrplem  18287  pgpfac1lem3  18299  irredrmul  18530  islbs3  18976  lbsextlem3  18981  lbsextlem4  18982  rng1nfld  19099  mvrf1  19246  f1lindf  19980  perfopn  20799  pnfnei  20834  mnfnei  20835  haust1  20966  cmpcld  21015  ptbasfi  21194  fbncp  21453  isfild  21472  fbasfip  21482  filufint  21534  rnelfmlem  21566  fmfnfm  21572  fclscf  21639  ptcmplem3  21668  opnsubg  21721  bldisj  22013  iccntr  22432  icccmplem2  22434  reconnlem1  22437  reconnlem2  22438  evth  22566  lebnumlem3  22570  ovolicc2lem3  23094  volfiniun  23122  iundisj  23123  dvne0  23578  lhop2  23582  itgsubstlem  23615  coemullem  23810  plyexmo  23872  logccne0  24129  lgamgulmlem1  24555  wilthlem2  24595  wilth  24597  mumul  24707  chtublem  24736  perfect1  24753  lgsdilem2  24858  lgsne0  24860  lgsqrlem2  24872  lgseisenlem1  24900  lgseisenlem2  24901  lgsquadlem1  24905  lgsquadlem2  24906  lgsquadlem3  24907  lgsquad2lem1  24909  2sqblem  24956  chebbnd1lem1  24958  pntpbnd2  25076  pntlem3  25098  ostth  25128  umgrnloop0  25775  vdgr1a  26433  chirredlem1  28633  iundisjf  28784  ofpreima2  28849  iundisjfi  28942  fundmpss  30910  dfon2lem4  30935  dfon2lem7  30938  sltval2  31053  sltasym  31071  broutsideof2  31399  outsidele  31409  nn0prpwlem  31487  nn0prpw  31488  onint1  31618  fin2so  32566  poimirlem16  32595  lpssat  33318  exatleN  33708  3noncolr2  33753  4noncolr3  33757  3dimlem3  33765  3dimlem3OLDN  33766  3dimlem4a  33767  3dimlem4  33768  3dimlem4OLDN  33769  3atlem4  33790  3atlem5  33791  3atlem6  33792  llnnleat  33817  lplnnle2at  33845  lvolnle3at  33886  4atlem0a  33897  4atlem0ae  33898  dalem21  33998  dalem54  34030  cdlemblem  34097  lhpmcvr4N  34330  4atexlemnclw  34374  cdlemd3  34505  cdleme3g  34539  cdleme3h  34540  cdleme7aa  34547  cdleme7d  34551  cdleme7ga  34553  cdleme11c  34566  cdleme15b  34580  cdleme20zN  34606  cdleme20yOLD  34608  cdleme21b  34632  cdleme21c  34633  cdleme21ct  34635  cdleme22b  34647  cdleme32b  34748  cdleme35fnpq  34755  cdleme35f  34760  cdleme36a  34766  cdleme42c  34778  cdleme48bw  34808  cdlemf1  34867  cdlemg2fv2  34906  cdlemg7fvbwN  34913  cdlemg4  34923  cdlemg6c  34926  cdlemg27a  34998  cdlemg27b  35002  cdlemk3  35139  dia2dimlem1  35371  dihord6apre  35563  dihord6b  35567  dihord5apre  35569  dihglbcpreN  35607  dihmeetlem6  35616  dochnel2  35699  dochexmidlem7  35773  lspindp5  36077  mapdh8b  36087  hdmapip0  36225  pellexlem6  36416  elpell14qr2  36444  pellfundglb  36467  jm2.19  36578  jm2.26lem3  36586  setindtr  36609  harinf  36619  dgraa0p  36738  gneispace0nelrn3  37460  fpropnf1  40337  usgrnloop0ALT  40432  1wlkp1lem2  40883  pthdlem2lem  40973