Theorem mtand 816

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 412	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1, 3	mtod 198	1 ⊢ (𝜑 → ¬ 𝜓)

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

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 207  df-an 396

This theorem is referenced by:  mteqand  3030  nelpr2  4657  nelpr1  4658  peano5  7915  wfrlem16OLD  8362  cofonr  8710  sdomnsym  9136  domnsymfi  9237  unxpdomlem2  9284  cnfcom2lem  9738  cflim2  10300  fin23lem39  10387  isf32lem2  10391  konigthlem  10605  pythagtriplem4  16852  pythagtriplem11  16858  pythagtriplem13  16860  prmreclem1  16949  smndex2dnrinv  18940  psgnunilem5  19526  sylow1lem3  19632  efgredlema  19772  efgredlemc  19777  rrgnz  20720  lssvancl1  20960  lspexchn1  21149  lspindp1  21152  zringlpirlem3  21492  evlslem3  22121  reconnlem2  24862  aaliou2  26396  logdmnrp  26697  dmgmaddnn0  27084  2sqcoprm  27493  pntpbnd1  27644  ostth2lem4  27694  nosepssdm  27745  nolt02olem  27753  nolt02o  27754  nogt01o  27755  nosupbnd1lem3  27769  nosupbnd1lem4  27770  nosupbnd1lem5  27771  nosupbnd1lem6  27772  noinfbnd1lem3  27784  noinfbnd1lem4  27785  noinfbnd1lem5  27786  noinfbnd1lem6  27787  nocvxminlem  27836  ssltdisj  27880  sltlpss  27959  cofcutr  27972  sltmul2  28211  ncolcom  28583  ncolrot1  28584  ncolrot2  28585  ncoltgdim2  28587  hleqnid  28630  ncolne1  28647  ncolncol  28668  miriso  28692  mirbtwnhl  28702  symquadlem  28711  ragncol  28731  mideulem2  28756  oppne3  28765  opphllem1  28769  opphllem2  28770  opphllem4  28772  opphl  28776  hpgerlem  28787  lmieu  28806  cgrancol  28851  fracfld  33289  rhmpreimaprmidl  33458  qsnzr  33462  krullndrng  33488  rsprprmprmidl  33529  0ringirng  33703  lmdvg  33913  ballotlemfcc  34474  ballotlemi1  34483  ballotlemii  34484  tgoldbachgtda  34654  prv0  35414  lindsenlbs  37601  mblfinlem1  37643  lcvnbtwn  39006  ncvr1  39253  lnnat  39409  lplncvrlvol  39598  dalem39  39693  lhpocnle  39998  cdleme17b  40269  cdlemg31c  40681  lclkrlem2o  41503  lcfrlem19  41543  baerlem5amN  41698  baerlem5bmN  41699  baerlem5abmN  41700  mapdh8ab  41759  mapdh8ad  41761  mapdh8c  41763  oexpreposd  42335  nelsubginvcld  42482  nelsubgcld  42483  fphpd  42803  fiphp3d  42806  pellexlem6  42821  elpell1qr2  42859  pellqrex  42866  pellfund14gap  42874  unxpwdom3  43083  elnelneqd  44191  elnelneq2d  44192  dvgrat  44307  limcperiod  45583  sumnnodd  45585  stirlinglem5  46033  dirkercncflem2  46059  fourierdlem25  46087  fourierdlem63  46124  elaa2  46189  etransclem9  46198  etransclem41  46230  etransclem44  46233  preimagelt  46654  preimalegt  46655