Theorem mtand 827

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

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

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 210  df-an 401

This theorem is referenced by:  mteqand  3049  elnelneqd  3057  elnelneq2d  3058  nelpr2  4620  nelpr1  4621  peano5  7891  cofonr  8661  sdomnsym  9091  domnsymfi  9185  unxpdomlem2  9218  cnfcom2lem  9671  cflim2  10248  fin23lem39  10335  isf32lem2  10339  konigthlem  10554  pythagtriplem4  16880  pythagtriplem11  16886  pythagtriplem13  16888  prmreclem1  16977  smndex2dnrinv  18978  psgnunilem5  19565  sylow1lem3  19671  efgredlema  19811  efgredlemc  19816  rrgnz  20790  lssvancl1  21047  lspexchn1  21235  lspindp1  21238  rhmpreimaprmidl  21460  qsnzr  21464  prmidlsubm  21468  zringlpirlem3  21595  evlslem3  22212  reconnlem2  24966  aaliou2  26484  logdmnrp  26787  dmgmaddnn0  27172  2sqcoprm  27580  pntpbnd1  27731  ostth2lem4  27781  nosepssdm  27831  nolt02olem  27839  nolt02o  27840  nogt01o  27841  nosupbnd1lem3  27855  nosupbnd1lem4  27856  nosupbnd1lem5  27857  nosupbnd1lem6  27858  noinfbnd1lem3  27870  noinfbnd1lem4  27871  noinfbnd1lem5  27872  noinfbnd1lem6  27873  nocvxminlem  27928  sltsdisj  27977  eqcuts3  27978  ltslpss  28082  cofcutr  28098  ltmuls2  28345  bdayfinbndlem1  28641  z12bdaylem1  28644  ncolcom  28811  ncolrot1  28812  ncolrot2  28813  ncoltgdim2  28815  hleqnid  28861  ncolne1  28879  ncolncol  28901  tglnpt4  28909  miriso  28928  mirbtwnhl  28938  symquadlem  28947  symquadprlnglem  28951  ragncol  28970  mideulem2  28996  oppne3  29005  opphllem1  29009  opphllem2  29010  opphllem4  29012  opphl  29016  oppmir  29017  hpgerlem  29028  lnincplng  29047  plngrotlem1  29050  plngrotlem2  29051  lnssplnglem  29054  lnssplng  29055  nhpmirhp  29061  lmieu  29074  cgrancol  29121  dfprlng2  29178  prlngex  29182  prlngmolem1  29183  prlngmolem2  29184  prlnginn0  29191  prlngmid2  29192  prlngsymquadopp  29196  quadcgrprlng  29197  fracfld  33610  krullndrng  33744  dflringlem2  33766  dflring3  33768  rsprprmprmidl  33793  esplymhp  33939  0ringirng  34060  constrcon  34145  lmdvg  34324  ballotlemfcc  34865  ballotlemi1  34874  ballotlemii  34875  tgoldbachgtda  35029  morleylemrneab  35039  prv0  35903  ttcwf2  37017  lindsenlbs  38247  mblfinlem1  38289  lcvnbtwn  39780  ncvr1  40027  lnnat  40182  lplncvrlvol  40371  dalem39  40466  lhpocnle  40771  cdleme17b  41042  cdlemg31c  41454  lclkrlem2o  42276  lcfrlem19  42316  baerlem5amN  42471  baerlem5bmN  42472  baerlem5abmN  42473  mapdh8ab  42532  mapdh8ad  42534  mapdh8c  42536  oexpreposd  43064  mullt0b2d  43239  nelsubginvcld  43251  nelsubgcld  43252  fphpd  43526  fiphp3d  43529  pellexlem6  43544  elpell1qr2  43582  pellqrex  43589  pellfund14gap  43597  unxpwdom3  43805  dvgrat  45005  limcperiod  46327  sumnnodd  46329  stirlinglem5  46775  dirkercncflem2  46801  fourierdlem25  46829  fourierdlem63  46866  elaa2  46931  etransclem9  46940  etransclem41  46972  etransclem44  46975  preimagelt  47396  preimalegt  47397  nelsubc2  49830