MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mtand Structured version   Visualization version   GIF version

Theorem mtand 688
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
StepHypRef Expression
1 mtand.1 . 2 (𝜑 → ¬ 𝜒)
2 mtand.2 . . 3 ((𝜑𝜓) → 𝜒)
32ex 448 . 2 (𝜑 → (𝜓𝜒))
41, 3mtod 187 1 (𝜑 → ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  peano5  6959  wfrlem16  7295  sdomnsym  7948  unxpdomlem2  8028  cnfcom2lem  8459  cflim2  8946  fin23lem39  9033  isf32lem2  9037  konigthlem  9247  pythagtriplem4  15311  pythagtriplem11  15317  pythagtriplem13  15319  prmreclem1  15407  psgnunilem5  17686  sylow1lem3  17787  efgredlema  17925  efgredlemc  17930  lssvancl1  18715  lspexchn1  18900  lspindp1  18903  evlslem3  19284  zringlpirlem3  19602  reconnlem2  22386  aaliou2  23844  logdmnrp  24132  dmgmaddnn0  24498  pntpbnd1  25020  ostth2lem4  25070  ncolcom  25202  ncolrot1  25203  ncolrot2  25204  ncoltgdim2  25206  hleqnid  25249  ncolne1  25266  ncolncol  25287  miriso  25311  mirbtwnhl  25321  symquadlem  25330  ragncol  25350  mideulem2  25372  opphllem4  25388  opphl  25392  hpgerlem  25403  lmieu  25422  2sqcoprm  28812  lmdvg  29161  ballotlemfcc  29716  ballotlemi1  29725  ballotlemii  29726  nocvxminlem  30923  lindsenlbs  32398  mblfinlem1  32440  lcvnbtwn  33154  ncvr1  33401  lnnat  33555  lplncvrlvol  33744  dalem39  33839  lhpocnle  34144  cdleme17b  34416  cdlemg31c  34829  lclkrlem2o  35652  lcfrlem19  35692  baerlem5amN  35847  baerlem5bmN  35848  baerlem5abmN  35849  mapdh8ab  35908  mapdh8ad  35910  mapdh8c  35912  fphpd  36222  fiphp3d  36225  pellexlem6  36240  elpell1qr2  36278  pellqrex  36285  pellfund14gap  36293  unxpwdom3  36507  dvgrat  37357  limcperiod  38519  sumnnodd  38521  stirlinglem5  38795  dirkercncflem2  38821  fourierdlem25  38849  fourierdlem63  38886  elaa2  38951  etransclem9  38960  etransclem41  38992  etransclem44  38995
  Copyright terms: Public domain W3C validator