Theorem mtand 812

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 197	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 206  df-an 396

This theorem is referenced by:  mteqand  3047  nelpr2  4585  nelpr1  4586  peano5  7714  peano5OLD  7715  wfrlem16OLD  8126  sdomnsym  8838  unxpdomlem2  8957  cnfcom2lem  9389  cflim2  9950  fin23lem39  10037  isf32lem2  10041  konigthlem  10255  pythagtriplem4  16448  pythagtriplem11  16454  pythagtriplem13  16456  prmreclem1  16545  smndex2dnrinv  18469  psgnunilem5  19017  sylow1lem3  19120  efgredlema  19261  efgredlemc  19266  lssvancl1  20121  lspexchn1  20307  lspindp1  20310  zringlpirlem3  20598  evlslem3  21200  reconnlem2  23896  aaliou2  25405  logdmnrp  25701  dmgmaddnn0  26081  2sqcoprm  26488  pntpbnd1  26639  ostth2lem4  26689  ncolcom  26826  ncolrot1  26827  ncolrot2  26828  ncoltgdim2  26830  hleqnid  26873  ncolne1  26890  ncolncol  26911  miriso  26935  mirbtwnhl  26945  symquadlem  26954  ragncol  26974  mideulem2  26999  oppne3  27008  opphllem1  27012  opphllem2  27013  opphllem4  27015  opphl  27019  hpgerlem  27030  lmieu  27049  cgrancol  27094  rhmpreimaprmidl  31529  lmdvg  31805  ballotlemfcc  32360  ballotlemi1  32369  ballotlemii  32370  tgoldbachgtda  32541  prv0  33292  nosepssdm  33816  nolt02olem  33824  nolt02o  33825  nogt01o  33826  nosupbnd1lem3  33840  nosupbnd1lem4  33841  nosupbnd1lem5  33842  nosupbnd1lem6  33843  noinfbnd1lem3  33855  noinfbnd1lem4  33856  noinfbnd1lem5  33857  noinfbnd1lem6  33858  nocvxminlem  33899  ssltdisj  33942  sltlpss  34014  cofcutr  34019  lindsenlbs  35699  mblfinlem1  35741  lcvnbtwn  36966  ncvr1  37213  lnnat  37368  lplncvrlvol  37557  dalem39  37652  lhpocnle  37957  cdleme17b  38228  cdlemg31c  38640  lclkrlem2o  39462  lcfrlem19  39502  baerlem5amN  39657  baerlem5bmN  39658  baerlem5abmN  39659  mapdh8ab  39718  mapdh8ad  39720  mapdh8c  39722  nelsubginvcld  40146  nelsubgcld  40147  oexpreposd  40242  fphpd  40554  fiphp3d  40557  pellexlem6  40572  elpell1qr2  40610  pellqrex  40617  pellfund14gap  40625  unxpwdom3  40836  elnelneqd  41702  elnelneq2d  41703  dvgrat  41819  limcperiod  43059  sumnnodd  43061  stirlinglem5  43509  dirkercncflem2  43535  fourierdlem25  43563  fourierdlem63  43600  elaa2  43665  etransclem9  43674  etransclem41  43706  etransclem44  43709  preimagelt  44126  preimalegt  44127