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  3023  nelpr2  4610  nelpr1  4611  peano5  7835  cofonr  8602  sdomnsym  9030  domnsymfi  9124  unxpdomlem2  9157  cnfcom2lem  9610  cflim2  10173  fin23lem39  10260  isf32lem2  10264  konigthlem  10479  pythagtriplem4  16747  pythagtriplem11  16753  pythagtriplem13  16755  prmreclem1  16844  smndex2dnrinv  18840  psgnunilem5  19423  sylow1lem3  19529  efgredlema  19669  efgredlemc  19674  rrgnz  20637  lssvancl1  20896  lspexchn1  21085  lspindp1  21088  zringlpirlem3  21419  evlslem3  22035  reconnlem2  24772  aaliou2  26304  logdmnrp  26606  dmgmaddnn0  26993  2sqcoprm  27402  pntpbnd1  27553  ostth2lem4  27603  nosepssdm  27654  nolt02olem  27662  nolt02o  27663  nogt01o  27664  nosupbnd1lem3  27678  nosupbnd1lem4  27679  nosupbnd1lem5  27680  nosupbnd1lem6  27681  noinfbnd1lem3  27693  noinfbnd1lem4  27694  noinfbnd1lem5  27695  noinfbnd1lem6  27696  nocvxminlem  27750  sltsdisj  27799  eqcuts3  27800  ltslpss  27904  cofcutr  27920  ltmuls2  28167  bdayfinbndlem1  28463  z12bdaylem1  28466  ncolcom  28633  ncolrot1  28634  ncolrot2  28635  ncoltgdim2  28637  hleqnid  28680  ncolne1  28697  ncolncol  28718  miriso  28742  mirbtwnhl  28752  symquadlem  28761  ragncol  28781  mideulem2  28806  oppne3  28815  opphllem1  28819  opphllem2  28820  opphllem4  28822  opphl  28826  hpgerlem  28837  lmieu  28856  cgrancol  28901  fracfld  33390  rhmpreimaprmidl  33532  qsnzr  33536  krullndrng  33562  rsprprmprmidl  33603  esplymhp  33726  0ringirng  33846  constrcon  33931  lmdvg  34110  ballotlemfcc  34651  ballotlemi1  34660  ballotlemii  34661  tgoldbachgtda  34818  prv0  35624  lindsenlbs  37812  mblfinlem1  37854  lcvnbtwn  39281  ncvr1  39528  lnnat  39683  lplncvrlvol  39872  dalem39  39967  lhpocnle  40272  cdleme17b  40543  cdlemg31c  40955  lclkrlem2o  41777  lcfrlem19  41817  baerlem5amN  41972  baerlem5bmN  41973  baerlem5abmN  41974  mapdh8ab  42033  mapdh8ad  42035  mapdh8c  42037  oexpreposd  42573  mullt0b2d  42735  nelsubginvcld  42747  nelsubgcld  42748  fphpd  43054  fiphp3d  43057  pellexlem6  43072  elpell1qr2  43110  pellqrex  43117  pellfund14gap  43125  unxpwdom3  43333  elnelneqd  44439  elnelneq2d  44440  dvgrat  44549  limcperiod  45870  sumnnodd  45872  stirlinglem5  46318  dirkercncflem2  46344  fourierdlem25  46372  fourierdlem63  46409  elaa2  46474  etransclem9  46483  etransclem41  46515  etransclem44  46518  preimagelt  46939  preimalegt  46940  nelsubc2  49310