Theorem mtand 821

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

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

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 208  df-an 397

This theorem is referenced by:  mteqand  3026  nelpr2  4592  nelpr1  4593  peano5  7840  cofonr  8607  sdomnsym  9037  domnsymfi  9131  unxpdomlem2  9164  cnfcom2lem  9620  cflim2  10183  fin23lem39  10270  isf32lem2  10274  konigthlem  10489  pythagtriplem4  16788  pythagtriplem11  16794  pythagtriplem13  16796  prmreclem1  16885  smndex2dnrinv  18884  psgnunilem5  19467  sylow1lem3  19573  efgredlema  19713  efgredlemc  19718  rrgnz  20683  lssvancl1  20942  lspexchn1  21130  lspindp1  21133  zringlpirlem3  21446  evlslem3  22063  reconnlem2  24818  aaliou2  26331  logdmnrp  26630  dmgmaddnn0  27015  2sqcoprm  27423  pntpbnd1  27574  ostth2lem4  27624  nosepssdm  27675  nolt02olem  27683  nolt02o  27684  nogt01o  27685  nosupbnd1lem3  27699  nosupbnd1lem4  27700  nosupbnd1lem5  27701  nosupbnd1lem6  27702  noinfbnd1lem3  27714  noinfbnd1lem4  27715  noinfbnd1lem5  27716  noinfbnd1lem6  27717  nocvxminlem  27771  sltsdisj  27820  eqcuts3  27821  ltslpss  27925  cofcutr  27941  ltmuls2  28188  bdayfinbndlem1  28484  z12bdaylem1  28487  ncolcom  28654  ncolrot1  28655  ncolrot2  28656  ncoltgdim2  28658  hleqnid  28701  ncolne1  28718  ncolncol  28739  miriso  28763  mirbtwnhl  28773  symquadlem  28782  ragncol  28802  mideulem2  28827  oppne3  28836  opphllem1  28840  opphllem2  28841  opphllem4  28843  opphl  28847  hpgerlem  28858  lmieu  28877  cgrancol  28922  fracfld  33399  rhmpreimaprmidl  33541  qsnzr  33545  krullndrng  33571  rsprprmprmidl  33612  esplymhp  33759  0ringirng  33880  constrcon  33965  lmdvg  34144  ballotlemfcc  34685  ballotlemi1  34694  ballotlemii  34695  tgoldbachgtda  34852  prv0  35665  ttcwf2  36760  lindsenlbs  37989  mblfinlem1  38031  lcvnbtwn  39524  ncvr1  39771  lnnat  39926  lplncvrlvol  40115  dalem39  40210  lhpocnle  40515  cdleme17b  40786  cdlemg31c  41198  lclkrlem2o  42020  lcfrlem19  42060  baerlem5amN  42215  baerlem5bmN  42216  baerlem5abmN  42217  mapdh8ab  42276  mapdh8ad  42278  mapdh8c  42280  oexpreposd  42806  mullt0b2d  42981  nelsubginvcld  42993  nelsubgcld  42994  fphpd  43268  fiphp3d  43271  pellexlem6  43286  elpell1qr2  43324  pellqrex  43331  pellfund14gap  43339  unxpwdom3  43547  elnelneqd  44653  elnelneq2d  44654  dvgrat  44763  limcperiod  46080  sumnnodd  46082  stirlinglem5  46528  dirkercncflem2  46554  fourierdlem25  46582  fourierdlem63  46619  elaa2  46684  etransclem9  46693  etransclem41  46725  etransclem44  46728  preimagelt  47149  preimalegt  47150  nelsubc2  49566