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  3016  nelpr2  4617  nelpr1  4618  peano5  7869  cofonr  8638  sdomnsym  9066  domnsymfi  9164  unxpdomlem2  9198  cnfcom2lem  9654  cflim2  10216  fin23lem39  10303  isf32lem2  10307  konigthlem  10521  pythagtriplem4  16790  pythagtriplem11  16796  pythagtriplem13  16798  prmreclem1  16887  smndex2dnrinv  18842  psgnunilem5  19424  sylow1lem3  19530  efgredlema  19670  efgredlemc  19675  rrgnz  20613  lssvancl1  20851  lspexchn1  21040  lspindp1  21043  zringlpirlem3  21374  evlslem3  21987  reconnlem2  24716  aaliou2  26248  logdmnrp  26550  dmgmaddnn0  26937  2sqcoprm  27346  pntpbnd1  27497  ostth2lem4  27547  nosepssdm  27598  nolt02olem  27606  nolt02o  27607  nogt01o  27608  nosupbnd1lem3  27622  nosupbnd1lem4  27623  nosupbnd1lem5  27624  nosupbnd1lem6  27625  noinfbnd1lem3  27637  noinfbnd1lem4  27638  noinfbnd1lem5  27639  noinfbnd1lem6  27640  nocvxminlem  27689  ssltdisj  27733  sltlpss  27819  cofcutr  27832  sltmul2  28074  ncolcom  28488  ncolrot1  28489  ncolrot2  28490  ncoltgdim2  28492  hleqnid  28535  ncolne1  28552  ncolncol  28573  miriso  28597  mirbtwnhl  28607  symquadlem  28616  ragncol  28636  mideulem2  28661  oppne3  28670  opphllem1  28674  opphllem2  28675  opphllem4  28677  opphl  28681  hpgerlem  28692  lmieu  28711  cgrancol  28756  fracfld  33258  rhmpreimaprmidl  33422  qsnzr  33426  krullndrng  33452  rsprprmprmidl  33493  0ringirng  33684  constrcon  33764  lmdvg  33943  ballotlemfcc  34485  ballotlemi1  34494  ballotlemii  34495  tgoldbachgtda  34652  prv0  35417  lindsenlbs  37609  mblfinlem1  37651  lcvnbtwn  39018  ncvr1  39265  lnnat  39421  lplncvrlvol  39610  dalem39  39705  lhpocnle  40010  cdleme17b  40281  cdlemg31c  40693  lclkrlem2o  41515  lcfrlem19  41555  baerlem5amN  41710  baerlem5bmN  41711  baerlem5abmN  41712  mapdh8ab  41771  mapdh8ad  41773  mapdh8c  41775  oexpreposd  42310  mullt0b2d  42472  nelsubginvcld  42484  nelsubgcld  42485  fphpd  42804  fiphp3d  42807  pellexlem6  42822  elpell1qr2  42860  pellqrex  42867  pellfund14gap  42875  unxpwdom3  43084  elnelneqd  44191  elnelneq2d  44192  dvgrat  44301  limcperiod  45626  sumnnodd  45628  stirlinglem5  46076  dirkercncflem2  46102  fourierdlem25  46130  fourierdlem63  46167  elaa2  46232  etransclem9  46241  etransclem41  46273  etransclem44  46276  preimagelt  46697  preimalegt  46698  nelsubc2  49058