Theorem mtand 804

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

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

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 199  df-an 388

This theorem is referenced by:  nelpr2  4461  nelpr1  4462  peano5  7419  wfrlem16  7773  sdomnsym  8437  unxpdomlem2  8517  cnfcom2lem  8957  cflim2  9482  fin23lem39  9569  isf32lem2  9573  konigthlem  9787  pythagtriplem4  16011  pythagtriplem11  16017  pythagtriplem13  16019  prmreclem1  16107  psgnunilem5  18396  psgnunilem5OLD  18397  sylow1lem3  18499  efgredlema  18638  efgredlemc  18643  lssvancl1  19451  lspexchn1  19637  lspindp1  19640  evlslem3  20020  zringlpirlem3  20351  reconnlem2  23154  aaliou2  24648  logdmnrp  24941  dmgmaddnn0  25322  2sqcoprm  25729  pntpbnd1  25880  ostth2lem4  25930  ncolcom  26065  ncolrot1  26066  ncolrot2  26067  ncoltgdim2  26069  hleqnid  26112  ncolne1  26129  ncolncol  26150  miriso  26174  mirbtwnhl  26184  symquadlem  26193  ragncol  26213  mideulem2  26238  oppne3  26247  opphllem1  26251  opphllem2  26252  opphllem4  26254  opphl  26258  hpgerlem  26269  lmieu  26288  cgrancol  26333  lmdvg  30873  ballotlemfcc  31430  ballotlemi1  31439  ballotlemii  31440  tgoldbachgtda  31613  nosepssdm  32744  nolt02olem  32752  nolt02o  32753  nosupbnd1lem3  32764  nosupbnd1lem4  32765  nosupbnd1lem5  32766  nosupbnd1lem6  32767  nocvxminlem  32801  lindsenlbs  34361  mblfinlem1  34403  lcvnbtwn  35639  ncvr1  35886  lnnat  36041  lplncvrlvol  36230  dalem39  36325  lhpocnle  36630  cdleme17b  36901  cdlemg31c  37313  lclkrlem2o  38135  lcfrlem19  38175  baerlem5amN  38330  baerlem5bmN  38331  baerlem5abmN  38332  mapdh8ab  38391  mapdh8ad  38393  mapdh8c  38395  mteqand  38582  nelsubginvcld  38607  nelsubgcld  38608  oexpreposd  38645  fphpd  38843  fiphp3d  38846  pellexlem6  38861  elpell1qr2  38899  pellqrex  38906  pellfund14gap  38914  unxpwdom3  39125  elnelneqd  39953  elnelneq2d  39954  dvgrat  40094  limcperiod  41370  sumnnodd  41372  stirlinglem5  41824  dirkercncflem2  41850  fourierdlem25  41878  fourierdlem63  41915  elaa2  41980  etransclem9  41989  etransclem41  42021  etransclem44  42024  preimagelt  42441  preimalegt  42442