Theorem mtand 689

Description: A modus tollens deduction. (Contributed by Jeff Hankins, 19-Aug-2009.)

Hypotheses

Ref	Expression
mtand.1	⊢ (𝜑 → ¬ 𝜒)
mtand.2	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
mtand	⊢ (𝜑 → ¬ 𝜓)

Proof of Theorem mtand

Step	Hyp	Ref	Expression
1		mtand.1	. 2 ⊢ (𝜑 → ¬ 𝜒)
2		mtand.2	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3	2	ex 449	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1, 3	mtod 188	1 ⊢ (𝜑 → ¬ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 196  df-an 385

This theorem is referenced by:  peano5  6981  wfrlem16  7317  sdomnsym  7970  unxpdomlem2  8050  cnfcom2lem  8481  cflim2  8968  fin23lem39  9055  isf32lem2  9059  konigthlem  9269  pythagtriplem4  15362  pythagtriplem11  15368  pythagtriplem13  15370  prmreclem1  15458  psgnunilem5  17737  sylow1lem3  17838  efgredlema  17976  efgredlemc  17981  lssvancl1  18766  lspexchn1  18951  lspindp1  18954  evlslem3  19335  zringlpirlem3  19653  reconnlem2  22438  aaliou2  23899  logdmnrp  24187  dmgmaddnn0  24553  pntpbnd1  25075  ostth2lem4  25125  ncolcom  25256  ncolrot1  25257  ncolrot2  25258  ncoltgdim2  25260  hleqnid  25303  ncolne1  25320  ncolncol  25341  miriso  25365  mirbtwnhl  25375  symquadlem  25384  ragncol  25404  mideulem2  25426  opphllem4  25442  opphl  25446  hpgerlem  25457  lmieu  25476  2sqcoprm  28978  lmdvg  29327  ballotlemfcc  29882  ballotlemi1  29891  ballotlemii  29892  nocvxminlem  31089  lindsenlbs  32574  mblfinlem1  32616  lcvnbtwn  33330  ncvr1  33577  lnnat  33731  lplncvrlvol  33920  dalem39  34015  lhpocnle  34320  cdleme17b  34592  cdlemg31c  35005  lclkrlem2o  35828  lcfrlem19  35868  baerlem5amN  36023  baerlem5bmN  36024  baerlem5abmN  36025  mapdh8ab  36084  mapdh8ad  36086  mapdh8c  36088  fphpd  36398  fiphp3d  36401  pellexlem6  36416  elpell1qr2  36454  pellqrex  36461  pellfund14gap  36469  unxpwdom3  36683  dvgrat  37533  limcperiod  38695  sumnnodd  38697  stirlinglem5  38971  dirkercncflem2  38997  fourierdlem25  39025  fourierdlem63  39062  elaa2  39127  etransclem9  39136  etransclem41  39168  etransclem44  39171