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  3020  nelpr2  4605  nelpr1  4606  peano5  7829  cofonr  8595  sdomnsym  9022  domnsymfi  9116  unxpdomlem2  9148  cnfcom2lem  9598  cflim2  10161  fin23lem39  10248  isf32lem2  10252  konigthlem  10466  pythagtriplem4  16733  pythagtriplem11  16739  pythagtriplem13  16741  prmreclem1  16830  smndex2dnrinv  18825  psgnunilem5  19408  sylow1lem3  19514  efgredlema  19654  efgredlemc  19659  rrgnz  20621  lssvancl1  20880  lspexchn1  21069  lspindp1  21072  zringlpirlem3  21403  evlslem3  22016  reconnlem2  24744  aaliou2  26276  logdmnrp  26578  dmgmaddnn0  26965  2sqcoprm  27374  pntpbnd1  27525  ostth2lem4  27575  nosepssdm  27626  nolt02olem  27634  nolt02o  27635  nogt01o  27636  nosupbnd1lem3  27650  nosupbnd1lem4  27651  nosupbnd1lem5  27652  nosupbnd1lem6  27653  noinfbnd1lem3  27665  noinfbnd1lem4  27666  noinfbnd1lem5  27667  noinfbnd1lem6  27668  nocvxminlem  27718  ssltdisj  27765  eqscut3  27766  sltlpss  27854  cofcutr  27869  sltmul2  28111  ncolcom  28540  ncolrot1  28541  ncolrot2  28542  ncoltgdim2  28544  hleqnid  28587  ncolne1  28604  ncolncol  28625  miriso  28649  mirbtwnhl  28659  symquadlem  28668  ragncol  28688  mideulem2  28713  oppne3  28722  opphllem1  28726  opphllem2  28727  opphllem4  28729  opphl  28733  hpgerlem  28744  lmieu  28763  cgrancol  28808  fracfld  33281  rhmpreimaprmidl  33423  qsnzr  33427  krullndrng  33453  rsprprmprmidl  33494  esplymhp  33608  0ringirng  33723  constrcon  33808  lmdvg  33987  ballotlemfcc  34528  ballotlemi1  34537  ballotlemii  34538  tgoldbachgtda  34695  prv0  35495  lindsenlbs  37675  mblfinlem1  37717  lcvnbtwn  39144  ncvr1  39391  lnnat  39546  lplncvrlvol  39735  dalem39  39830  lhpocnle  40135  cdleme17b  40406  cdlemg31c  40818  lclkrlem2o  41640  lcfrlem19  41680  baerlem5amN  41835  baerlem5bmN  41836  baerlem5abmN  41837  mapdh8ab  41896  mapdh8ad  41898  mapdh8c  41900  oexpreposd  42440  mullt0b2d  42602  nelsubginvcld  42614  nelsubgcld  42615  fphpd  42933  fiphp3d  42936  pellexlem6  42951  elpell1qr2  42989  pellqrex  42996  pellfund14gap  43004  unxpwdom3  43212  elnelneqd  44319  elnelneq2d  44320  dvgrat  44429  limcperiod  45752  sumnnodd  45754  stirlinglem5  46200  dirkercncflem2  46226  fourierdlem25  46254  fourierdlem63  46291  elaa2  46356  etransclem9  46365  etransclem41  46397  etransclem44  46400  preimagelt  46821  preimalegt  46822  nelsubc2  49194