Theorem mtand 815

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  3019  nelpr2  4606  nelpr1  4607  peano5  7823  cofonr  8589  sdomnsym  9015  domnsymfi  9109  unxpdomlem2  9141  cnfcom2lem  9591  cflim2  10151  fin23lem39  10238  isf32lem2  10242  konigthlem  10456  pythagtriplem4  16728  pythagtriplem11  16734  pythagtriplem13  16736  prmreclem1  16825  smndex2dnrinv  18820  psgnunilem5  19404  sylow1lem3  19510  efgredlema  19650  efgredlemc  19655  rrgnz  20617  lssvancl1  20876  lspexchn1  21065  lspindp1  21068  zringlpirlem3  21399  evlslem3  22013  reconnlem2  24741  aaliou2  26273  logdmnrp  26575  dmgmaddnn0  26962  2sqcoprm  27371  pntpbnd1  27522  ostth2lem4  27572  nosepssdm  27623  nolt02olem  27631  nolt02o  27632  nogt01o  27633  nosupbnd1lem3  27647  nosupbnd1lem4  27648  nosupbnd1lem5  27649  nosupbnd1lem6  27650  noinfbnd1lem3  27662  noinfbnd1lem4  27663  noinfbnd1lem5  27664  noinfbnd1lem6  27665  nocvxminlem  27715  ssltdisj  27762  eqscut3  27763  sltlpss  27851  cofcutr  27866  sltmul2  28108  ncolcom  28537  ncolrot1  28538  ncolrot2  28539  ncoltgdim2  28541  hleqnid  28584  ncolne1  28601  ncolncol  28622  miriso  28646  mirbtwnhl  28656  symquadlem  28665  ragncol  28685  mideulem2  28710  oppne3  28719  opphllem1  28723  opphllem2  28724  opphllem4  28726  opphl  28730  hpgerlem  28741  lmieu  28760  cgrancol  28805  fracfld  33269  rhmpreimaprmidl  33411  qsnzr  33415  krullndrng  33441  rsprprmprmidl  33482  esplymhp  33584  0ringirng  33697  constrcon  33782  lmdvg  33961  ballotlemfcc  34502  ballotlemi1  34511  ballotlemii  34512  tgoldbachgtda  34669  prv0  35462  lindsenlbs  37654  mblfinlem1  37696  lcvnbtwn  39063  ncvr1  39310  lnnat  39465  lplncvrlvol  39654  dalem39  39749  lhpocnle  40054  cdleme17b  40325  cdlemg31c  40737  lclkrlem2o  41559  lcfrlem19  41599  baerlem5amN  41754  baerlem5bmN  41755  baerlem5abmN  41756  mapdh8ab  41815  mapdh8ad  41817  mapdh8c  41819  oexpreposd  42354  mullt0b2d  42516  nelsubginvcld  42528  nelsubgcld  42529  fphpd  42848  fiphp3d  42851  pellexlem6  42866  elpell1qr2  42904  pellqrex  42911  pellfund14gap  42919  unxpwdom3  43127  elnelneqd  44234  elnelneq2d  44235  dvgrat  44344  limcperiod  45667  sumnnodd  45669  stirlinglem5  46115  dirkercncflem2  46141  fourierdlem25  46169  fourierdlem63  46206  elaa2  46271  etransclem9  46280  etransclem41  46312  etransclem44  46315  preimagelt  46736  preimalegt  46737  nelsubc2  49100