Theorem mtod 190

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 188	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  191  mtbid  316  mtbird  317  mtand  804  mtord  864  po2nr  5343  po3nr  5344  ordn2lp  6054  ordnbtwn  6124  fpropnf1  6856  tfi  7390  nnlim  7415  smoord  7812  tz7.48-3  7889  oalimcl  7993  omlimcl  8011  oneo  8014  omopth2  8017  nnneo  8084  mapdom2  8490  php3  8505  onomeneq  8509  sucdom2  8515  isfinite2  8577  domunfican  8592  ordtypelem7  8789  unxpwdom2  8853  cantnfp1lem2  8942  oemapvali  8947  cantnflem1  8952  cantnflem2  8953  rankpwi  9052  tskwe  9179  alephordi  9300  alephdom  9307  cardaleph  9315  cflim2  9489  isfin4p1  9541  fin23lem26  9551  fin1a2lem13  9638  axcclem  9683  fpwwe2lem12  9867  fpwwe2lem13  9868  fpwwe2  9869  pwxpndom2  9891  pwxpndom  9892  pwdjundom  9893  gchaleph  9897  r1wunlim  9963  inatsk  10004  tskuni  10009  gruina  10044  prlem934  10259  dedekind  10609  prodge0rd  12319  qextltlem  12418  ixxub  12581  ixxlb  12582  seqf1olem1  13230  facndiv  13469  cnpart  14466  rlimuni  14774  rlimcld2  14802  isercoll  14891  incexclem  15057  isumltss  15069  alzdvds  15536  fzm1ndvds  15538  fzo0dvdseq  15539  bitsfzolem  15649  smuval2  15697  smupvallem  15698  bezoutlem3  15751  rpdvds  15866  nonsq  15961  prmdiv  15984  odzdvds  15994  pcprendvds  16039  pcprendvds2  16040  pcpremul  16042  pcdvdsb  16067  pcadd2  16088  pockthlem  16103  prmreclem5  16118  prmreclem6  16119  1arith  16125  4sqlem11  16153  vdwlem11  16189  vdwlem12  16190  ramubcl  16216  mrissmrcd  16781  pltnlt  17448  acsfiindd  17657  odcl2  18465  gexnnod  18486  pgpssslw  18512  torsubg  18742  lt6abl  18781  ablfacrplem  18949  pgpfac1lem3  18961  irredrmul  19192  islbs3  19661  lbsextlem3  19666  lbsextlem4  19667  rng1nfld  19784  mvrf1  19931  f1lindf  20683  perfopn  21512  pnfnei  21547  mnfnei  21548  haust1  21679  cmpcld  21729  ptbasfi  21908  fbncp  22166  isfild  22185  fbasfip  22195  filufint  22247  rnelfmlem  22279  fmfnfm  22285  fclscf  22352  ptcmplem3  22381  opnsubg  22434  bldisj  22726  iccntr  23147  icccmplem2  23149  reconnlem1  23152  reconnlem2  23153  evth  23281  lebnumlem3  23285  ovolicc2lem3  23838  volfiniun  23866  iundisj  23867  dvne0  24326  lhop2  24330  itgsubstlem  24363  coemullem  24558  plyexmo  24620  logccne0  24878  lgamgulmlem1  25323  wilthlem2  25363  wilth  25365  mumul  25475  chtublem  25504  perfect1  25521  lgsdilem2  25626  lgsne0  25628  lgsqrlem2  25640  lgseisenlem1  25668  lgseisenlem2  25669  lgsquadlem1  25673  lgsquadlem2  25674  lgsquadlem3  25675  lgsquad2lem1  25677  2sqblem  25724  chebbnd1lem1  25762  pntpbnd2  25880  pntlem3  25902  ostth  25932  umgrnloop0  26612  usgrnloop0ALT  26705  wlkp1lem2  27177  pthdlem2lem  27271  chirredlem1  29963  iundisjf  30122  ofpreima2  30190  iundisjfi  30292  fundmpss  32569  dfon2lem4  32591  dfon2lem7  32594  frrlem14  32697  sltval2  32724  nolt02o  32760  nosupbnd1lem2  32770  nosupbnd1  32775  nosupbnd2  32777  noetalem3  32780  broutsideof2  33144  outsidele  33154  nn0prpwlem  33231  onint1  33357  fin2so  34360  lindsadd  34366  poimirlem16  34389  lpssat  35634  exatleN  36025  3noncolr2  36070  4noncolr3  36074  3dimlem3  36082  3dimlem3OLDN  36083  3dimlem4a  36084  3dimlem4  36085  3dimlem4OLDN  36086  3atlem4  36107  3atlem5  36108  3atlem6  36109  llnnleat  36134  lplnnle2at  36162  lvolnle3at  36203  4atlem0a  36214  4atlem0ae  36215  dalem21  36315  dalem54  36347  cdlemblem  36414  lhpmcvr4N  36647  4atexlemnclw  36691  cdlemd3  36821  cdleme3g  36855  cdleme3h  36856  cdleme7aa  36863  cdleme7d  36867  cdleme7ga  36869  cdleme11c  36882  cdleme15b  36896  cdleme20zN  36922  cdleme21b  36947  cdleme21c  36948  cdleme21ct  36950  cdleme22b  36962  cdleme32b  37063  cdleme35fnpq  37070  cdleme35f  37075  cdleme36a  37081  cdleme42c  37093  cdleme48bw  37123  cdlemf1  37182  cdlemg2fv2  37221  cdlemg7fvbwN  37228  cdlemg4  37238  cdlemg6c  37241  cdlemg27a  37313  cdlemg27b  37317  cdlemk3  37454  dia2dimlem1  37685  dihord6apre  37877  dihord6b  37881  dihord5apre  37883  dihglbcpreN  37921  dihmeetlem6  37930  dochnel2  38013  dochexmidlem7  38087  lspindp5  38391  mapdh8b  38401  hdmapip0  38536  rtprmirr  38667  pellexlem6  38868  elpell14qr2  38896  pellfundglb  38919  jm2.19  39027  jm2.26lem3  39035  setindtr  39058  harinf  39068  dgraa0p  39186  gneispace0nelrn3  39896  ablsimpnosubgd  40081