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  5546  po3nr  5547  ordn2lp  6337  ordnbtwn  6412  fpropnf1  7213  tfi  7795  nnlim  7822  frrlem14  8241  smoord  8297  tz7.48-3  8375  oalimcl  8487  omlimcl  8505  oneo  8508  omopth2  8511  nnneo  8583  mapdom2  9076  sucdom2  9127  php2  9132  1sdom2dom  9154  isfinite2  9198  domunfican  9222  ordtypelem7  9429  unxpwdom2  9493  cantnfp1lem2  9588  oemapvali  9593  cantnflem1  9598  cantnflem2  9599  rankpwi  9735  tskwe  9862  alephordi  9984  alephdom  9991  cardaleph  9999  cflim2  10173  isfin4p1  10225  fin23lem26  10235  fin1a2lem13  10322  axcclem  10367  fpwwe2lem11  10552  fpwwe2lem12  10553  fpwwe2  10554  pwxpndom2  10576  pwxpndom  10577  pwdjundom  10578  gchaleph  10582  r1wunlim  10648  inatsk  10689  tskuni  10694  gruina  10729  prlem934  10944  dedekind  11296  prodge0rd  13014  qextltlem  13117  ixxub  13282  ixxlb  13283  seqf1olem1  13964  facndiv  14211  cnpart  15163  rlimuni  15473  rlimcld2  15501  isercoll  15591  incexclem  15759  isumltss  15771  alzdvds  16247  fzm1ndvds  16249  fzo0dvdseq  16250  bitsfzolem  16361  smuval2  16409  smupvallem  16410  bezoutlem3  16468  rpdvds  16587  nonsq  16686  prmdiv  16712  odzdvds  16723  pcprendvds  16768  pcprendvds2  16769  pcpremul  16771  pcdvdsb  16797  pcadd2  16818  pockthlem  16833  prmreclem5  16848  prmreclem6  16849  1arith  16855  4sqlem11  16883  vdwlem11  16919  vdwlem12  16920  ramubcl  16946  mrissmrcd  17563  pltnlt  18261  acsfiindd  18476  odcl2  19494  gexnnod  19517  pgpssslw  19543  torsubg  19783  lt6abl  19824  ablfacrplem  19996  pgpfac1lem3  20008  ablsimpnosubgd  20035  irredrmul  20363  islbs3  21110  lbsextlem3  21115  lbsextlem4  21116  f1lindf  21777  mvrf1  21941  psdmul  22109  perfopn  23129  pnfnei  23164  mnfnei  23165  haust1  23296  cmpcld  23346  ptbasfi  23525  fbncp  23783  isfild  23802  fbasfip  23812  filufint  23864  rnelfmlem  23896  fmfnfm  23902  fclscf  23969  ptcmplem3  23998  opnsubg  24052  bldisj  24342  iccntr  24766  icccmplem2  24768  reconnlem1  24771  reconnlem2  24772  evth  24914  lebnumlem3  24918  ovolicc2lem3  25476  volfiniun  25504  iundisj  25505  dvne0  25972  lhop2  25976  itgsubstlem  26011  coemullem  26211  plyexmo  26277  logccne0  26543  rtprmirr  26726  lgamgulmlem1  26995  wilthlem2  27035  wilth  27037  mumul  27147  chtublem  27178  perfect1  27195  lgsdilem2  27300  lgsne0  27302  lgsqrlem2  27314  lgseisenlem1  27342  lgseisenlem2  27343  lgsquadlem1  27347  lgsquadlem2  27348  lgsquadlem3  27349  lgsquad2lem1  27351  2sqblem  27398  chebbnd1lem1  27436  pntpbnd2  27554  pntlem3  27576  ostth  27606  ltsval2  27624  nolt02o  27663  nosupbnd1lem2  27677  nosupbnd1  27682  nosupbnd2  27684  noinfbnd1lem2  27692  noinfbnd1  27697  noinfbnd2  27699  noetasuplem4  27704  noetainflem4  27708  cutbdaybnd2lim  27793  oniso  28267  bdayfinbndlem1  28463  z12bdaylem1  28466  umgrnloop0  29182  usgrnloop0ALT  29278  wlkp1lem2  29746  pthdlem2lem  29840  chirredlem1  32465  iundisjf  32664  ofpreima2  32744  iundisjfi  32876  rprmndvdsru  33610  antnest  35883  antnestlaw3lem  35884  fundmpss  35961  dfon2lem4  35978  dfon2lem7  35981  broutsideof2  36316  outsidele  36326  nn0prpwlem  36516  onint1  36643  fin2so  37804  lindsadd  37810  lpssat  39269  exatleN  39660  3noncolr2  39705  4noncolr3  39709  3dimlem3  39717  3dimlem3OLDN  39718  3dimlem4a  39719  3dimlem4  39720  3dimlem4OLDN  39721  3atlem4  39742  3atlem5  39743  3atlem6  39744  llnnleat  39769  lplnnle2at  39797  lvolnle3at  39838  4atlem0a  39849  4atlem0ae  39850  dalem21  39950  dalem54  39982  cdlemblem  40049  lhpmcvr4N  40282  4atexlemnclw  40326  cdlemd3  40456  cdleme3g  40490  cdleme3h  40491  cdleme7aa  40498  cdleme7d  40502  cdleme7ga  40504  cdleme11c  40517  cdleme15b  40531  cdleme20zN  40557  cdleme21b  40582  cdleme21c  40583  cdleme21ct  40585  cdleme22b  40597  cdleme32b  40698  cdleme35fnpq  40705  cdleme35f  40710  cdleme36a  40716  cdleme42c  40728  cdleme48bw  40758  cdlemf1  40817  cdlemg2fv2  40856  cdlemg7fvbwN  40863  cdlemg4  40873  cdlemg6c  40876  cdlemg27a  40948  cdlemg27b  40952  cdlemk3  41089  dia2dimlem1  41320  dihord6apre  41512  dihord6b  41516  dihord5apre  41518  dihglbcpreN  41556  dihmeetlem6  41565  dochnel2  41648  dochexmidlem7  41722  lspindp5  42026  mapdh8b  42036  hdmapip0  42171  aks6d1c2p2  42369  flt4lem5elem  42890  flt4lem7  42898  nna4b4nsq  42899  pellexlem6  43072  elpell14qr2  43100  pellfundglb  43123  jm2.19  43231  jm2.26lem3  43239  setindtr  43262  harinf  43272  dgraa0p  43387  tfsconcatb0  43582  gneispace0nelrn3  44379