Theorem mtod 200

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 198	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  201  mtbid  326  mtbird  327  mtand  814  mtord  876  po2nr  5489  po3nr  5490  ordn2lp  6213  ordnbtwn  6283  fpropnf1  7027  tfi  7570  nnlim  7595  smoord  8004  tz7.48-3  8082  oalimcl  8188  omlimcl  8206  oneo  8209  omopth2  8212  nnneo  8280  mapdom2  8690  php3  8705  onomeneq  8710  sucdom2  8716  isfinite2  8778  domunfican  8793  ordtypelem7  8990  unxpwdom2  9054  cantnfp1lem2  9144  oemapvali  9149  cantnflem1  9154  cantnflem2  9155  rankpwi  9254  tskwe  9381  alephordi  9502  alephdom  9509  cardaleph  9517  cflim2  9687  isfin4p1  9739  fin23lem26  9749  fin1a2lem13  9836  axcclem  9881  fpwwe2lem12  10065  fpwwe2lem13  10066  fpwwe2  10067  pwxpndom2  10089  pwxpndom  10090  pwdjundom  10091  gchaleph  10095  r1wunlim  10161  inatsk  10202  tskuni  10207  gruina  10242  prlem934  10457  dedekind  10805  prodge0rd  12499  qextltlem  12598  ixxub  12762  ixxlb  12763  seqf1olem1  13412  facndiv  13651  cnpart  14601  rlimuni  14909  rlimcld2  14937  isercoll  15026  incexclem  15193  isumltss  15205  alzdvds  15672  fzm1ndvds  15674  fzo0dvdseq  15675  bitsfzolem  15785  smuval2  15833  smupvallem  15834  bezoutlem3  15891  rpdvds  16006  nonsq  16101  prmdiv  16124  odzdvds  16134  pcprendvds  16179  pcprendvds2  16180  pcpremul  16182  pcdvdsb  16207  pcadd2  16228  pockthlem  16243  prmreclem5  16258  prmreclem6  16259  1arith  16265  4sqlem11  16293  vdwlem11  16329  vdwlem12  16330  ramubcl  16356  mrissmrcd  16913  pltnlt  17580  acsfiindd  17789  odcl2  18694  gexnnod  18715  pgpssslw  18741  torsubg  18976  lt6abl  19017  ablfacrplem  19189  pgpfac1lem3  19201  ablsimpnosubgd  19228  irredrmul  19459  islbs3  19929  lbsextlem3  19934  lbsextlem4  19935  rng1nfld  20053  mvrf1  20207  f1lindf  20968  perfopn  21795  pnfnei  21830  mnfnei  21831  haust1  21962  cmpcld  22012  ptbasfi  22191  fbncp  22449  isfild  22468  fbasfip  22478  filufint  22530  rnelfmlem  22562  fmfnfm  22568  fclscf  22635  ptcmplem3  22664  opnsubg  22718  bldisj  23010  iccntr  23431  icccmplem2  23433  reconnlem1  23436  reconnlem2  23437  evth  23565  lebnumlem3  23569  ovolicc2lem3  24122  volfiniun  24150  iundisj  24151  dvne0  24610  lhop2  24614  itgsubstlem  24647  coemullem  24842  plyexmo  24904  logccne0  25164  lgamgulmlem1  25608  wilthlem2  25648  wilth  25650  mumul  25760  chtublem  25789  perfect1  25806  lgsdilem2  25911  lgsne0  25913  lgsqrlem2  25925  lgseisenlem1  25953  lgseisenlem2  25954  lgsquadlem1  25958  lgsquadlem2  25959  lgsquadlem3  25960  lgsquad2lem1  25962  2sqblem  26009  chebbnd1lem1  26047  pntpbnd2  26165  pntlem3  26187  ostth  26217  umgrnloop0  26896  usgrnloop0ALT  26989  wlkp1lem2  27458  pthdlem2lem  27550  chirredlem1  30169  iundisjf  30341  ofpreima2  30413  iundisjfi  30521  fundmpss  33011  dfon2lem4  33033  dfon2lem7  33036  frrlem14  33138  sltval2  33165  nolt02o  33201  nosupbnd1lem2  33211  nosupbnd1  33216  nosupbnd2  33218  noetalem3  33221  broutsideof2  33585  outsidele  33595  nn0prpwlem  33672  onint1  33799  fin2so  34881  lindsadd  34887  poimirlem16  34910  lpssat  36151  exatleN  36542  3noncolr2  36587  4noncolr3  36591  3dimlem3  36599  3dimlem3OLDN  36600  3dimlem4a  36601  3dimlem4  36602  3dimlem4OLDN  36603  3atlem4  36624  3atlem5  36625  3atlem6  36626  llnnleat  36651  lplnnle2at  36679  lvolnle3at  36720  4atlem0a  36731  4atlem0ae  36732  dalem21  36832  dalem54  36864  cdlemblem  36931  lhpmcvr4N  37164  4atexlemnclw  37208  cdlemd3  37338  cdleme3g  37372  cdleme3h  37373  cdleme7aa  37380  cdleme7d  37384  cdleme7ga  37386  cdleme11c  37399  cdleme15b  37413  cdleme20zN  37439  cdleme21b  37464  cdleme21c  37465  cdleme21ct  37467  cdleme22b  37479  cdleme32b  37580  cdleme35fnpq  37587  cdleme35f  37592  cdleme36a  37598  cdleme42c  37610  cdleme48bw  37640  cdlemf1  37699  cdlemg2fv2  37738  cdlemg7fvbwN  37745  cdlemg4  37755  cdlemg6c  37758  cdlemg27a  37830  cdlemg27b  37834  cdlemk3  37971  dia2dimlem1  38202  dihord6apre  38394  dihord6b  38398  dihord5apre  38400  dihglbcpreN  38438  dihmeetlem6  38447  dochnel2  38530  dochexmidlem7  38604  lspindp5  38908  mapdh8b  38918  hdmapip0  39053  rtprmirr  39201  pellexlem6  39438  elpell14qr2  39466  pellfundglb  39489  jm2.19  39597  jm2.26lem3  39605  setindtr  39628  harinf  39638  dgraa0p  39756  gneispace0nelrn3  40499