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  5545  po3nr  5546  ordn2lp  6331  ordnbtwn  6406  fpropnf1  7208  tfi  7793  nnlim  7820  frrlem14  8239  smoord  8295  tz7.48-3  8373  oalimcl  8485  omlimcl  8503  oneo  8506  omopth2  8509  nnneo  8580  mapdom2  9072  sucdom2  9127  php2  9132  1sdom2dom  9153  isfinite2  9203  domunfican  9230  ordtypelem7  9435  unxpwdom2  9499  cantnfp1lem2  9594  oemapvali  9599  cantnflem1  9604  cantnflem2  9605  rankpwi  9738  tskwe  9865  alephordi  9987  alephdom  9994  cardaleph  10002  cflim2  10176  isfin4p1  10228  fin23lem26  10238  fin1a2lem13  10325  axcclem  10370  fpwwe2lem11  10554  fpwwe2lem12  10555  fpwwe2  10556  pwxpndom2  10578  pwxpndom  10579  pwdjundom  10580  gchaleph  10584  r1wunlim  10650  inatsk  10691  tskuni  10696  gruina  10731  prlem934  10946  dedekind  11297  prodge0rd  13020  qextltlem  13122  ixxub  13287  ixxlb  13288  seqf1olem1  13966  facndiv  14213  cnpart  15165  rlimuni  15475  rlimcld2  15503  isercoll  15593  incexclem  15761  isumltss  15773  alzdvds  16249  fzm1ndvds  16251  fzo0dvdseq  16252  bitsfzolem  16363  smuval2  16411  smupvallem  16412  bezoutlem3  16470  rpdvds  16589  nonsq  16688  prmdiv  16714  odzdvds  16725  pcprendvds  16770  pcprendvds2  16771  pcpremul  16773  pcdvdsb  16799  pcadd2  16820  pockthlem  16835  prmreclem5  16850  prmreclem6  16851  1arith  16857  4sqlem11  16885  vdwlem11  16921  vdwlem12  16922  ramubcl  16948  mrissmrcd  17564  pltnlt  18262  acsfiindd  18477  odcl2  19462  gexnnod  19485  pgpssslw  19511  torsubg  19751  lt6abl  19792  ablfacrplem  19964  pgpfac1lem3  19976  ablsimpnosubgd  20003  irredrmul  20330  islbs3  21080  lbsextlem3  21085  lbsextlem4  21086  f1lindf  21747  mvrf1  21911  psdmul  22069  perfopn  23088  pnfnei  23123  mnfnei  23124  haust1  23255  cmpcld  23305  ptbasfi  23484  fbncp  23742  isfild  23761  fbasfip  23771  filufint  23823  rnelfmlem  23855  fmfnfm  23861  fclscf  23928  ptcmplem3  23957  opnsubg  24011  bldisj  24302  iccntr  24726  icccmplem2  24728  reconnlem1  24731  reconnlem2  24732  evth  24874  lebnumlem3  24878  ovolicc2lem3  25436  volfiniun  25464  iundisj  25465  dvne0  25932  lhop2  25936  itgsubstlem  25971  coemullem  26171  plyexmo  26237  logccne0  26503  rtprmirr  26686  lgamgulmlem1  26955  wilthlem2  26995  wilth  26997  mumul  27107  chtublem  27138  perfect1  27155  lgsdilem2  27260  lgsne0  27262  lgsqrlem2  27274  lgseisenlem1  27302  lgseisenlem2  27303  lgsquadlem1  27307  lgsquadlem2  27308  lgsquadlem3  27309  lgsquad2lem1  27311  2sqblem  27358  chebbnd1lem1  27396  pntpbnd2  27514  pntlem3  27536  ostth  27566  sltval2  27584  nolt02o  27623  nosupbnd1lem2  27637  nosupbnd1  27642  nosupbnd2  27644  noinfbnd1lem2  27652  noinfbnd1  27657  noinfbnd2  27659  noetasuplem4  27664  noetainflem4  27668  scutbdaybnd2lim  27746  onsiso  28192  umgrnloop0  29072  usgrnloop0ALT  29168  wlkp1lem2  29636  pthdlem2lem  29730  chirredlem1  32352  iundisjf  32551  ofpreima2  32623  iundisjfi  32752  rprmndvdsru  33476  antnest  35661  antnestlaw3lem  35662  fundmpss  35739  dfon2lem4  35759  dfon2lem7  35762  broutsideof2  36095  outsidele  36105  nn0prpwlem  36295  onint1  36422  fin2so  37586  lindsadd  37592  lpssat  38991  exatleN  39383  3noncolr2  39428  4noncolr3  39432  3dimlem3  39440  3dimlem3OLDN  39441  3dimlem4a  39442  3dimlem4  39443  3dimlem4OLDN  39444  3atlem4  39465  3atlem5  39466  3atlem6  39467  llnnleat  39492  lplnnle2at  39520  lvolnle3at  39561  4atlem0a  39572  4atlem0ae  39573  dalem21  39673  dalem54  39705  cdlemblem  39772  lhpmcvr4N  40005  4atexlemnclw  40049  cdlemd3  40179  cdleme3g  40213  cdleme3h  40214  cdleme7aa  40221  cdleme7d  40225  cdleme7ga  40227  cdleme11c  40240  cdleme15b  40254  cdleme20zN  40280  cdleme21b  40305  cdleme21c  40306  cdleme21ct  40308  cdleme22b  40320  cdleme32b  40421  cdleme35fnpq  40428  cdleme35f  40433  cdleme36a  40439  cdleme42c  40451  cdleme48bw  40481  cdlemf1  40540  cdlemg2fv2  40579  cdlemg7fvbwN  40586  cdlemg4  40596  cdlemg6c  40599  cdlemg27a  40671  cdlemg27b  40675  cdlemk3  40812  dia2dimlem1  41043  dihord6apre  41235  dihord6b  41239  dihord5apre  41241  dihglbcpreN  41279  dihmeetlem6  41288  dochnel2  41371  dochexmidlem7  41445  lspindp5  41749  mapdh8b  41759  hdmapip0  41894  aks6d1c2p2  42092  flt4lem5elem  42624  flt4lem7  42632  nna4b4nsq  42633  pellexlem6  42807  elpell14qr2  42835  pellfundglb  42858  jm2.19  42966  jm2.26lem3  42974  setindtr  42997  harinf  43007  dgraa0p  43122  tfsconcatb0  43317  gneispace0nelrn3  44115