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  3051  nelpr2  4615  nelpr1  4616  peano5  7878  cofonr  8648  sdomnsym  9078  domnsymfi  9172  unxpdomlem2  9205  cnfcom2lem  9658  cflim2  10235  fin23lem39  10322  isf32lem2  10326  konigthlem  10541  pythagtriplem4  16867  pythagtriplem11  16873  pythagtriplem13  16875  prmreclem1  16964  smndex2dnrinv  18965  psgnunilem5  19552  sylow1lem3  19658  efgredlema  19798  efgredlemc  19803  rrgnz  20777  lssvancl1  21032  lspexchn1  21220  lspindp1  21223  rhmpreimaprmidl  21436  qsnzr  21440  prmidlsubm  21444  zringlpirlem3  21571  evlslem3  22188  reconnlem2  24942  aaliou2  26458  logdmnrp  26760  dmgmaddnn0  27145  2sqcoprm  27553  pntpbnd1  27704  ostth2lem4  27754  nosepssdm  27804  nolt02olem  27812  nolt02o  27813  nogt01o  27814  nosupbnd1lem3  27828  nosupbnd1lem4  27829  nosupbnd1lem5  27830  nosupbnd1lem6  27831  noinfbnd1lem3  27843  noinfbnd1lem4  27844  noinfbnd1lem5  27845  noinfbnd1lem6  27846  nocvxminlem  27901  sltsdisj  27950  eqcuts3  27951  ltslpss  28055  cofcutr  28071  ltmuls2  28318  bdayfinbndlem1  28614  z12bdaylem1  28617  ncolcom  28784  ncolrot1  28785  ncolrot2  28786  ncoltgdim2  28788  hleqnid  28831  ncolne1  28848  ncolncol  28870  tglnpt4  28878  miriso  28897  mirbtwnhl  28907  symquadlem  28916  ragncol  28936  mideulem2  28961  oppne3  28970  opphllem1  28974  opphllem2  28975  opphllem4  28977  opphl  28981  hpgerlem  28992  lnincplng  29010  plngrotlem1  29013  plngrotlem2  29014  lnssplnglem  29017  lnssplng  29018  lmieu  29032  cgrancol  29077  fracfld  33539  krullndrng  33675  dflringlem2  33697  dflring3  33699  rsprprmprmidl  33724  esplymhp  33870  0ringirng  33991  constrcon  34076  lmdvg  34255  ballotlemfcc  34796  ballotlemi1  34805  ballotlemii  34806  tgoldbachgtda  34960  morleylemrneab  34970  prv0  35788  ttcwf2  36893  lindsenlbs  38121  mblfinlem1  38163  lcvnbtwn  39656  ncvr1  39903  lnnat  40058  lplncvrlvol  40247  dalem39  40342  lhpocnle  40647  cdleme17b  40918  cdlemg31c  41330  lclkrlem2o  42152  lcfrlem19  42192  baerlem5amN  42347  baerlem5bmN  42348  baerlem5abmN  42349  mapdh8ab  42408  mapdh8ad  42410  mapdh8c  42412  oexpreposd  42938  mullt0b2d  43113  nelsubginvcld  43125  nelsubgcld  43126  fphpd  43400  fiphp3d  43403  pellexlem6  43418  elpell1qr2  43456  pellqrex  43463  pellfund14gap  43471  unxpwdom3  43679  elnelneqd  44785  elnelneq2d  44786  dvgrat  44881  limcperiod  46203  sumnnodd  46205  stirlinglem5  46651  dirkercncflem2  46677  fourierdlem25  46705  fourierdlem63  46742  elaa2  46807  etransclem9  46816  etransclem41  46848  etransclem44  46851  preimagelt  47272  preimalegt  47273  nelsubc2  49699