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  3039  nelpr2  4675  nelpr1  4676  peano5  7932  peano5OLD  7933  wfrlem16OLD  8380  cofonr  8730  sdomnsym  9164  domnsymfi  9266  unxpdomlem2  9314  cnfcom2lem  9770  cflim2  10332  fin23lem39  10419  isf32lem2  10423  konigthlem  10637  pythagtriplem4  16866  pythagtriplem11  16872  pythagtriplem13  16874  prmreclem1  16963  smndex2dnrinv  18950  psgnunilem5  19536  sylow1lem3  19642  efgredlema  19782  efgredlemc  19787  rrgnz  20726  lssvancl1  20966  lspexchn1  21155  lspindp1  21158  zringlpirlem3  21498  evlslem3  22127  reconnlem2  24868  aaliou2  26400  logdmnrp  26701  dmgmaddnn0  27088  2sqcoprm  27497  pntpbnd1  27648  ostth2lem4  27698  nosepssdm  27749  nolt02olem  27757  nolt02o  27758  nogt01o  27759  nosupbnd1lem3  27773  nosupbnd1lem4  27774  nosupbnd1lem5  27775  nosupbnd1lem6  27776  noinfbnd1lem3  27788  noinfbnd1lem4  27789  noinfbnd1lem5  27790  noinfbnd1lem6  27791  nocvxminlem  27840  ssltdisj  27884  sltlpss  27963  cofcutr  27976  sltmul2  28215  ncolcom  28587  ncolrot1  28588  ncolrot2  28589  ncoltgdim2  28591  hleqnid  28634  ncolne1  28651  ncolncol  28672  miriso  28696  mirbtwnhl  28706  symquadlem  28715  ragncol  28735  mideulem2  28760  oppne3  28769  opphllem1  28773  opphllem2  28774  opphllem4  28776  opphl  28780  hpgerlem  28791  lmieu  28810  cgrancol  28855  fracfld  33275  rhmpreimaprmidl  33444  qsnzr  33448  krullndrng  33474  rsprprmprmidl  33515  0ringirng  33689  lmdvg  33899  ballotlemfcc  34458  ballotlemi1  34467  ballotlemii  34468  tgoldbachgtda  34638  prv0  35398  lindsenlbs  37575  mblfinlem1  37617  lcvnbtwn  38981  ncvr1  39228  lnnat  39384  lplncvrlvol  39573  dalem39  39668  lhpocnle  39973  cdleme17b  40244  cdlemg31c  40656  lclkrlem2o  41478  lcfrlem19  41518  baerlem5amN  41673  baerlem5bmN  41674  baerlem5abmN  41675  mapdh8ab  41734  mapdh8ad  41736  mapdh8c  41738  oexpreposd  42309  nelsubginvcld  42451  nelsubgcld  42452  fphpd  42772  fiphp3d  42775  pellexlem6  42790  elpell1qr2  42828  pellqrex  42835  pellfund14gap  42843  unxpwdom3  43052  elnelneqd  44164  elnelneq2d  44165  dvgrat  44281  limcperiod  45549  sumnnodd  45551  stirlinglem5  45999  dirkercncflem2  46025  fourierdlem25  46053  fourierdlem63  46090  elaa2  46155  etransclem9  46164  etransclem41  46196  etransclem44  46199  preimagelt  46620  preimalegt  46621