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 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  3024  nelpr2  4612  nelpr1  4613  peano5  7845  cofonr  8612  sdomnsym  9042  domnsymfi  9136  unxpdomlem2  9169  cnfcom2lem  9622  cflim2  10185  fin23lem39  10272  isf32lem2  10276  konigthlem  10491  pythagtriplem4  16759  pythagtriplem11  16765  pythagtriplem13  16767  prmreclem1  16856  smndex2dnrinv  18852  psgnunilem5  19435  sylow1lem3  19541  efgredlema  19681  efgredlemc  19686  rrgnz  20649  lssvancl1  20908  lspexchn1  21097  lspindp1  21100  zringlpirlem3  21431  evlslem3  22047  reconnlem2  24784  aaliou2  26316  logdmnrp  26618  dmgmaddnn0  27005  2sqcoprm  27414  pntpbnd1  27565  ostth2lem4  27615  nosepssdm  27666  nolt02olem  27674  nolt02o  27675  nogt01o  27676  nosupbnd1lem3  27690  nosupbnd1lem4  27691  nosupbnd1lem5  27692  nosupbnd1lem6  27693  noinfbnd1lem3  27705  noinfbnd1lem4  27706  noinfbnd1lem5  27707  noinfbnd1lem6  27708  nocvxminlem  27762  sltsdisj  27811  eqcuts3  27812  ltslpss  27916  cofcutr  27932  ltmuls2  28179  bdayfinbndlem1  28475  z12bdaylem1  28478  ncolcom  28645  ncolrot1  28646  ncolrot2  28647  ncoltgdim2  28649  hleqnid  28692  ncolne1  28709  ncolncol  28730  miriso  28754  mirbtwnhl  28764  symquadlem  28773  ragncol  28793  mideulem2  28818  oppne3  28827  opphllem1  28831  opphllem2  28832  opphllem4  28834  opphl  28838  hpgerlem  28849  lmieu  28868  cgrancol  28913  fracfld  33401  rhmpreimaprmidl  33543  qsnzr  33547  krullndrng  33573  rsprprmprmidl  33614  esplymhp  33744  0ringirng  33866  constrcon  33951  lmdvg  34130  ballotlemfcc  34671  ballotlemi1  34680  ballotlemii  34681  tgoldbachgtda  34838  prv0  35643  lindsenlbs  37860  mblfinlem1  37902  lcvnbtwn  39395  ncvr1  39642  lnnat  39797  lplncvrlvol  39986  dalem39  40081  lhpocnle  40386  cdleme17b  40657  cdlemg31c  41069  lclkrlem2o  41891  lcfrlem19  41931  baerlem5amN  42086  baerlem5bmN  42087  baerlem5abmN  42088  mapdh8ab  42147  mapdh8ad  42149  mapdh8c  42151  oexpreposd  42686  mullt0b2d  42848  nelsubginvcld  42860  nelsubgcld  42861  fphpd  43167  fiphp3d  43170  pellexlem6  43185  elpell1qr2  43223  pellqrex  43230  pellfund14gap  43238  unxpwdom3  43446  elnelneqd  44552  elnelneq2d  44553  dvgrat  44662  limcperiod  45982  sumnnodd  45984  stirlinglem5  46430  dirkercncflem2  46456  fourierdlem25  46484  fourierdlem63  46521  elaa2  46586  etransclem9  46595  etransclem41  46627  etransclem44  46630  preimagelt  47051  preimalegt  47052  nelsubc2  49422