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  4607  nelpr1  4608  peano5  7833  cofonr  8599  sdomnsym  9026  domnsymfi  9124  unxpdomlem2  9156  cnfcom2lem  9616  cflim2  10176  fin23lem39  10263  isf32lem2  10267  konigthlem  10481  pythagtriplem4  16749  pythagtriplem11  16755  pythagtriplem13  16757  prmreclem1  16846  smndex2dnrinv  18807  psgnunilem5  19391  sylow1lem3  19497  efgredlema  19637  efgredlemc  19642  rrgnz  20607  lssvancl1  20866  lspexchn1  21055  lspindp1  21058  zringlpirlem3  21389  evlslem3  22003  reconnlem2  24732  aaliou2  26264  logdmnrp  26566  dmgmaddnn0  26953  2sqcoprm  27362  pntpbnd1  27513  ostth2lem4  27563  nosepssdm  27614  nolt02olem  27622  nolt02o  27623  nogt01o  27624  nosupbnd1lem3  27638  nosupbnd1lem4  27639  nosupbnd1lem5  27640  nosupbnd1lem6  27641  noinfbnd1lem3  27653  noinfbnd1lem4  27654  noinfbnd1lem5  27655  noinfbnd1lem6  27656  nocvxminlem  27706  ssltdisj  27752  eqscut3  27753  sltlpss  27840  cofcutr  27855  sltmul2  28097  ncolcom  28524  ncolrot1  28525  ncolrot2  28526  ncoltgdim2  28528  hleqnid  28571  ncolne1  28588  ncolncol  28609  miriso  28633  mirbtwnhl  28643  symquadlem  28652  ragncol  28672  mideulem2  28697  oppne3  28706  opphllem1  28710  opphllem2  28711  opphllem4  28713  opphl  28717  hpgerlem  28728  lmieu  28747  cgrancol  28792  fracfld  33257  rhmpreimaprmidl  33398  qsnzr  33402  krullndrng  33428  rsprprmprmidl  33469  0ringirng  33660  constrcon  33740  lmdvg  33919  ballotlemfcc  34461  ballotlemi1  34470  ballotlemii  34471  tgoldbachgtda  34628  prv0  35402  lindsenlbs  37594  mblfinlem1  37636  lcvnbtwn  39003  ncvr1  39250  lnnat  39406  lplncvrlvol  39595  dalem39  39690  lhpocnle  39995  cdleme17b  40266  cdlemg31c  40678  lclkrlem2o  41500  lcfrlem19  41540  baerlem5amN  41695  baerlem5bmN  41696  baerlem5abmN  41697  mapdh8ab  41756  mapdh8ad  41758  mapdh8c  41760  oexpreposd  42295  mullt0b2d  42457  nelsubginvcld  42469  nelsubgcld  42470  fphpd  42789  fiphp3d  42792  pellexlem6  42807  elpell1qr2  42845  pellqrex  42852  pellfund14gap  42860  unxpwdom3  43068  elnelneqd  44175  elnelneq2d  44176  dvgrat  44285  limcperiod  45610  sumnnodd  45612  stirlinglem5  46060  dirkercncflem2  46086  fourierdlem25  46114  fourierdlem63  46151  elaa2  46216  etransclem9  46225  etransclem41  46257  etransclem44  46260  preimagelt  46681  preimalegt  46682  nelsubc2  49055