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  324  mtbird  325  mtand  813  mtord  877  po2nr  5518  po3nr  5519  ordn2lp  6290  ordnbtwn  6360  fpropnf1  7149  tfi  7709  nnlim  7735  frrlem14  8124  smoord  8205  tz7.48-3  8284  oalimcl  8400  omlimcl  8418  oneo  8421  omopth2  8424  nnneo  8494  sucdom2OLD  8878  mapdom2  8944  sucdom2  8998  php2  9003  php3OLD  9016  onomeneqOLD  9021  isfinite2  9081  domunfican  9096  ordtypelem7  9292  unxpwdom2  9356  cantnfp1lem2  9446  oemapvali  9451  cantnflem1  9456  cantnflem2  9457  rankpwi  9590  tskwe  9717  alephordi  9839  alephdom  9846  cardaleph  9854  cflim2  10028  isfin4p1  10080  fin23lem26  10090  fin1a2lem13  10177  axcclem  10222  fpwwe2lem11  10406  fpwwe2lem12  10407  fpwwe2  10408  pwxpndom2  10430  pwxpndom  10431  pwdjundom  10432  gchaleph  10436  r1wunlim  10502  inatsk  10543  tskuni  10548  gruina  10583  prlem934  10798  dedekind  11147  prodge0rd  12846  qextltlem  12945  ixxub  13109  ixxlb  13110  seqf1olem1  13771  facndiv  14011  cnpart  14960  rlimuni  15268  rlimcld2  15296  isercoll  15388  incexclem  15557  isumltss  15569  alzdvds  16038  fzm1ndvds  16040  fzo0dvdseq  16041  bitsfzolem  16150  smuval2  16198  smupvallem  16199  bezoutlem3  16258  rpdvds  16374  nonsq  16472  prmdiv  16495  odzdvds  16505  pcprendvds  16550  pcprendvds2  16551  pcpremul  16553  pcdvdsb  16579  pcadd2  16600  pockthlem  16615  prmreclem5  16630  prmreclem6  16631  1arith  16637  4sqlem11  16665  vdwlem11  16701  vdwlem12  16702  ramubcl  16728  mrissmrcd  17358  pltnlt  18067  acsfiindd  18280  odcl2  19181  gexnnod  19202  pgpssslw  19228  torsubg  19464  lt6abl  19505  ablfacrplem  19677  pgpfac1lem3  19689  ablsimpnosubgd  19716  irredrmul  19958  islbs3  20426  lbsextlem3  20431  lbsextlem4  20432  rng1nfld  20558  f1lindf  21038  mvrf1  21203  perfopn  22345  pnfnei  22380  mnfnei  22381  haust1  22512  cmpcld  22562  ptbasfi  22741  fbncp  22999  isfild  23018  fbasfip  23028  filufint  23080  rnelfmlem  23112  fmfnfm  23118  fclscf  23185  ptcmplem3  23214  opnsubg  23268  bldisj  23560  iccntr  23993  icccmplem2  23995  reconnlem1  23998  reconnlem2  23999  evth  24131  lebnumlem3  24135  ovolicc2lem3  24692  volfiniun  24720  iundisj  24721  dvne0  25184  lhop2  25188  itgsubstlem  25221  coemullem  25420  plyexmo  25482  logccne0  25743  lgamgulmlem1  26187  wilthlem2  26227  wilth  26229  mumul  26339  chtublem  26368  perfect1  26385  lgsdilem2  26490  lgsne0  26492  lgsqrlem2  26504  lgseisenlem1  26532  lgseisenlem2  26533  lgsquadlem1  26537  lgsquadlem2  26538  lgsquadlem3  26539  lgsquad2lem1  26541  2sqblem  26588  chebbnd1lem1  26626  pntpbnd2  26744  pntlem3  26766  ostth  26796  umgrnloop0  27488  usgrnloop0ALT  27581  wlkp1lem2  28051  pthdlem2lem  28144  chirredlem1  30761  iundisjf  30937  ofpreima2  31012  iundisjfi  31126  fundmpss  33749  dfon2lem4  33771  dfon2lem7  33774  sltval2  33868  nolt02o  33907  nosupbnd1lem2  33921  nosupbnd1  33926  nosupbnd2  33928  noinfbnd1lem2  33936  noinfbnd1  33941  noinfbnd2  33943  noetasuplem4  33948  noetainflem4  33952  scutbdaybnd2lim  34020  broutsideof2  34433  outsidele  34443  nn0prpwlem  34520  onint1  34647  fin2so  35773  lindsadd  35779  lpssat  37034  exatleN  37425  3noncolr2  37470  4noncolr3  37474  3dimlem3  37482  3dimlem3OLDN  37483  3dimlem4a  37484  3dimlem4  37485  3dimlem4OLDN  37486  3atlem4  37507  3atlem5  37508  3atlem6  37509  llnnleat  37534  lplnnle2at  37562  lvolnle3at  37603  4atlem0a  37614  4atlem0ae  37615  dalem21  37715  dalem54  37747  cdlemblem  37814  lhpmcvr4N  38047  4atexlemnclw  38091  cdlemd3  38221  cdleme3g  38255  cdleme3h  38256  cdleme7aa  38263  cdleme7d  38267  cdleme7ga  38269  cdleme11c  38282  cdleme15b  38296  cdleme20zN  38322  cdleme21b  38347  cdleme21c  38348  cdleme21ct  38350  cdleme22b  38362  cdleme32b  38463  cdleme35fnpq  38470  cdleme35f  38475  cdleme36a  38481  cdleme42c  38493  cdleme48bw  38523  cdlemf1  38582  cdlemg2fv2  38621  cdlemg7fvbwN  38628  cdlemg4  38638  cdlemg6c  38641  cdlemg27a  38713  cdlemg27b  38717  cdlemk3  38854  dia2dimlem1  39085  dihord6apre  39277  dihord6b  39281  dihord5apre  39283  dihglbcpreN  39321  dihmeetlem6  39330  dochnel2  39413  dochexmidlem7  39487  lspindp5  39791  mapdh8b  39801  hdmapip0  39936  rtprmirr  40354  flt4lem5elem  40495  flt4lem7  40503  nna4b4nsq  40504  pellexlem6  40663  elpell14qr2  40691  pellfundglb  40714  jm2.19  40822  jm2.26lem3  40830  setindtr  40853  harinf  40863  dgraa0p  40981  gneispace0nelrn3  41759