Theorem mtod 197

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 195	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  198  mtbid  323  mtbird  324  mtand  812  mtord  876  po2nr  5508  po3nr  5509  ordn2lp  6271  ordnbtwn  6341  fpropnf1  7121  tfi  7675  nnlim  7701  frrlem14  8086  smoord  8167  tz7.48-3  8245  oalimcl  8353  omlimcl  8371  oneo  8374  omopth2  8377  nnneo  8445  sucdom2  8822  mapdom2  8884  php3  8899  onomeneq  8943  isfinite2  9002  domunfican  9017  ordtypelem7  9213  unxpwdom2  9277  cantnfp1lem2  9367  oemapvali  9372  cantnflem1  9377  cantnflem2  9378  rankpwi  9512  tskwe  9639  alephordi  9761  alephdom  9768  cardaleph  9776  cflim2  9950  isfin4p1  10002  fin23lem26  10012  fin1a2lem13  10099  axcclem  10144  fpwwe2lem11  10328  fpwwe2lem12  10329  fpwwe2  10330  pwxpndom2  10352  pwxpndom  10353  pwdjundom  10354  gchaleph  10358  r1wunlim  10424  inatsk  10465  tskuni  10470  gruina  10505  prlem934  10720  dedekind  11068  prodge0rd  12766  qextltlem  12865  ixxub  13029  ixxlb  13030  seqf1olem1  13690  facndiv  13930  cnpart  14879  rlimuni  15187  rlimcld2  15215  isercoll  15307  incexclem  15476  isumltss  15488  alzdvds  15957  fzm1ndvds  15959  fzo0dvdseq  15960  bitsfzolem  16069  smuval2  16117  smupvallem  16118  bezoutlem3  16177  rpdvds  16293  nonsq  16391  prmdiv  16414  odzdvds  16424  pcprendvds  16469  pcprendvds2  16470  pcpremul  16472  pcdvdsb  16498  pcadd2  16519  pockthlem  16534  prmreclem5  16549  prmreclem6  16550  1arith  16556  4sqlem11  16584  vdwlem11  16620  vdwlem12  16621  ramubcl  16647  mrissmrcd  17266  pltnlt  17973  acsfiindd  18186  odcl2  19087  gexnnod  19108  pgpssslw  19134  torsubg  19370  lt6abl  19411  ablfacrplem  19583  pgpfac1lem3  19595  ablsimpnosubgd  19622  irredrmul  19864  islbs3  20332  lbsextlem3  20337  lbsextlem4  20338  rng1nfld  20462  f1lindf  20939  mvrf1  21104  perfopn  22244  pnfnei  22279  mnfnei  22280  haust1  22411  cmpcld  22461  ptbasfi  22640  fbncp  22898  isfild  22917  fbasfip  22927  filufint  22979  rnelfmlem  23011  fmfnfm  23017  fclscf  23084  ptcmplem3  23113  opnsubg  23167  bldisj  23459  iccntr  23890  icccmplem2  23892  reconnlem1  23895  reconnlem2  23896  evth  24028  lebnumlem3  24032  ovolicc2lem3  24588  volfiniun  24616  iundisj  24617  dvne0  25080  lhop2  25084  itgsubstlem  25117  coemullem  25316  plyexmo  25378  logccne0  25639  lgamgulmlem1  26083  wilthlem2  26123  wilth  26125  mumul  26235  chtublem  26264  perfect1  26281  lgsdilem2  26386  lgsne0  26388  lgsqrlem2  26400  lgseisenlem1  26428  lgseisenlem2  26429  lgsquadlem1  26433  lgsquadlem2  26434  lgsquadlem3  26435  lgsquad2lem1  26437  2sqblem  26484  chebbnd1lem1  26522  pntpbnd2  26640  pntlem3  26662  ostth  26692  umgrnloop0  27382  usgrnloop0ALT  27475  wlkp1lem2  27944  pthdlem2lem  28036  chirredlem1  30653  iundisjf  30829  ofpreima2  30905  iundisjfi  31019  fundmpss  33646  dfon2lem4  33668  dfon2lem7  33671  sltval2  33786  nolt02o  33825  nosupbnd1lem2  33839  nosupbnd1  33844  nosupbnd2  33846  noinfbnd1lem2  33854  noinfbnd1  33859  noinfbnd2  33861  noetasuplem4  33866  noetainflem4  33870  scutbdaybnd2lim  33938  broutsideof2  34351  outsidele  34361  nn0prpwlem  34438  onint1  34565  fin2so  35691  lindsadd  35697  lpssat  36954  exatleN  37345  3noncolr2  37390  4noncolr3  37394  3dimlem3  37402  3dimlem3OLDN  37403  3dimlem4a  37404  3dimlem4  37405  3dimlem4OLDN  37406  3atlem4  37427  3atlem5  37428  3atlem6  37429  llnnleat  37454  lplnnle2at  37482  lvolnle3at  37523  4atlem0a  37534  4atlem0ae  37535  dalem21  37635  dalem54  37667  cdlemblem  37734  lhpmcvr4N  37967  4atexlemnclw  38011  cdlemd3  38141  cdleme3g  38175  cdleme3h  38176  cdleme7aa  38183  cdleme7d  38187  cdleme7ga  38189  cdleme11c  38202  cdleme15b  38216  cdleme20zN  38242  cdleme21b  38267  cdleme21c  38268  cdleme21ct  38270  cdleme22b  38282  cdleme32b  38383  cdleme35fnpq  38390  cdleme35f  38395  cdleme36a  38401  cdleme42c  38413  cdleme48bw  38443  cdlemf1  38502  cdlemg2fv2  38541  cdlemg7fvbwN  38548  cdlemg4  38558  cdlemg6c  38561  cdlemg27a  38633  cdlemg27b  38637  cdlemk3  38774  dia2dimlem1  39005  dihord6apre  39197  dihord6b  39201  dihord5apre  39203  dihglbcpreN  39241  dihmeetlem6  39250  dochnel2  39333  dochexmidlem7  39407  lspindp5  39711  mapdh8b  39721  hdmapip0  39856  rtprmirr  40268  flt4lem5elem  40404  flt4lem7  40412  nna4b4nsq  40413  pellexlem6  40572  elpell14qr2  40600  pellfundglb  40623  jm2.19  40731  jm2.26lem3  40739  setindtr  40762  harinf  40772  dgraa0p  40890  gneispace0nelrn3  41641