Theorem mtand 828

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mteqand  3052  elnelneqd  3060  elnelneq2d  3061  nelpr2  4624  nelpr1  4625  peano5  7899  cofonr  8669  sdomnsym  9100  domnsymfi  9194  unxpdomlem2  9227  cnfcom2lem  9680  cflim2  10265  fin23lem39  10352  isf32lem2  10356  konigthlem  10571  pythagtriplem4  16904  pythagtriplem11  16910  pythagtriplem13  16912  prmreclem1  17001  smndex2dnrinv  19008  psgnunilem5  19595  sylow1lem3  19701  efgredlema  19841  efgredlemc  19846  rrgnz  20840  lssvancl1  21103  lspexchn1  21291  lspindp1  21294  rhmpreimaprmidl  21516  qsnzr  21520  prmidlsubm  21524  zringlpirlem3  21651  evlslem3  22268  reconnlem2  25022  aaliou2  26540  logdmnrp  26843  dmgmaddnn0  27228  2sqcoprm  27636  pntpbnd1  27787  ostth2lem4  27837  nosepssdm  27887  nolt02olem  27895  nolt02o  27896  nogt01o  27897  nosupbnd1lem3  27911  nosupbnd1lem4  27912  nosupbnd1lem5  27913  nosupbnd1lem6  27914  noinfbnd1lem3  27926  noinfbnd1lem4  27927  noinfbnd1lem5  27928  noinfbnd1lem6  27929  nocvxminlem  27984  sltsdisj  28033  eqcuts3  28034  ltslpss  28138  cofcutr  28154  ltmuls2  28401  bdayfinbndlem1  28697  z12bdaylem1  28700  ncolcom  28867  ncolrot1  28868  ncolrot2  28869  ncoltgdim2  28871  hleqnid  28917  ncolne1  28935  ncolncol  28957  tglnpt4  28965  miriso  28984  mirbtwnhl  28994  symquadlem  29003  symquadprlnglem  29007  ragncol  29026  mideulem2  29052  oppne3  29061  opphllem1  29065  opphllem2  29066  opphllem4  29068  opphl  29072  oppmir  29073  hpgerlem  29084  lnincplng  29103  plngrotlem1  29106  plngrotlem2  29107  lnssplnglem  29110  lnssplng  29111  nhpmirhp  29117  lmieu  29130  cgrancol  29177  dfprlng2  29234  prlngex  29238  prlngmolem1  29239  prlngmolem2  29240  prlnginn0  29247  prlngmid2  29248  prlngsymquadopp  29252  quadcgrprlng  29253  fracfld  33660  krullndrng  33794  dflringlem2  33816  dflring3  33818  rsprprmprmidl  33843  esplymhp  33989  0ringirng  34110  constrcon  34195  lmdvg  34374  ballotlemfcc  34916  ballotlemi1  34925  ballotlemii  34926  tgoldbachgtda  35080  morleylemrneab  35090  prv0  35943  ttcwf2  37077  lindsenlbs  38307  mblfinlem1  38349  lcvnbtwn  39840  ncvr1  40087  lnnat  40242  lplncvrlvol  40431  dalem39  40526  lhpocnle  40831  cdleme17b  41102  cdlemg31c  41514  lclkrlem2o  42336  lcfrlem19  42376  baerlem5amN  42531  baerlem5bmN  42532  baerlem5abmN  42533  mapdh8ab  42592  mapdh8ad  42594  mapdh8c  42596  oexpreposd  43124  mullt0b2d  43299  nelsubginvcld  43311  nelsubgcld  43312  fphpd  43584  fiphp3d  43587  pellexlem6  43602  elpell1qr2  43640  pellqrex  43647  pellfund14gap  43655  unxpwdom3  43863  dvgrat  45063  limcperiod  46385  sumnnodd  46387  stirlinglem5  46833  dirkercncflem2  46859  fourierdlem25  46887  fourierdlem63  46924  elaa2  46989  etransclem9  46998  etransclem41  47030  etransclem44  47033  preimagelt  47454  preimalegt  47455  nelsubc2  49888