Theorem mtand 816

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

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

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 210  df-an 400

This theorem is referenced by:  mteqand  3035  nelpr2  4554  nelpr1  4555  peano5  7649  peano5OLD  7650  wfrlem16  8048  sdomnsym  8749  unxpdomlem2  8859  cnfcom2lem  9294  cflim2  9842  fin23lem39  9929  isf32lem2  9933  konigthlem  10147  pythagtriplem4  16335  pythagtriplem11  16341  pythagtriplem13  16343  prmreclem1  16432  smndex2dnrinv  18296  psgnunilem5  18840  sylow1lem3  18943  efgredlema  19084  efgredlemc  19089  lssvancl1  19935  lspexchn1  20121  lspindp1  20124  zringlpirlem3  20405  evlslem3  20994  reconnlem2  23678  aaliou2  25187  logdmnrp  25483  dmgmaddnn0  25863  2sqcoprm  26270  pntpbnd1  26421  ostth2lem4  26471  ncolcom  26606  ncolrot1  26607  ncolrot2  26608  ncoltgdim2  26610  hleqnid  26653  ncolne1  26670  ncolncol  26691  miriso  26715  mirbtwnhl  26725  symquadlem  26734  ragncol  26754  mideulem2  26779  oppne3  26788  opphllem1  26792  opphllem2  26793  opphllem4  26795  opphl  26799  hpgerlem  26810  lmieu  26829  cgrancol  26874  rhmpreimaprmidl  31295  lmdvg  31571  ballotlemfcc  32126  ballotlemi1  32135  ballotlemii  32136  tgoldbachgtda  32307  prv0  33059  nosepssdm  33575  nolt02olem  33583  nolt02o  33584  nogt01o  33585  nosupbnd1lem3  33599  nosupbnd1lem4  33600  nosupbnd1lem5  33601  nosupbnd1lem6  33602  noinfbnd1lem3  33614  noinfbnd1lem4  33615  noinfbnd1lem5  33616  noinfbnd1lem6  33617  nocvxminlem  33658  ssltdisj  33701  sltlpss  33773  cofcutr  33778  lindsenlbs  35458  mblfinlem1  35500  lcvnbtwn  36725  ncvr1  36972  lnnat  37127  lplncvrlvol  37316  dalem39  37411  lhpocnle  37716  cdleme17b  37987  cdlemg31c  38399  lclkrlem2o  39221  lcfrlem19  39261  baerlem5amN  39416  baerlem5bmN  39417  baerlem5abmN  39418  mapdh8ab  39477  mapdh8ad  39479  mapdh8c  39481  nelsubginvcld  39874  nelsubgcld  39875  oexpreposd  39969  fphpd  40282  fiphp3d  40285  pellexlem6  40300  elpell1qr2  40338  pellqrex  40345  pellfund14gap  40353  unxpwdom3  40564  elnelneqd  41432  elnelneq2d  41433  dvgrat  41544  limcperiod  42787  sumnnodd  42789  stirlinglem5  43237  dirkercncflem2  43263  fourierdlem25  43291  fourierdlem63  43328  elaa2  43393  etransclem9  43402  etransclem41  43434  etransclem44  43437  preimagelt  43854  preimalegt  43855