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

Theorem mtand 641
Description: A modus tollens deduction. (Contributed by Jeff Hankins, 19-Aug-2009.)
Hypotheses
Ref Expression
mtand.1  |-  ( ph  ->  -.  ch )
mtand.2  |-  ( (
ph  /\  ps )  ->  ch )
Assertion
Ref Expression
mtand  |-  ( ph  ->  -.  ps )

Proof of Theorem mtand
StepHypRef Expression
1 mtand.1 . 2  |-  ( ph  ->  -.  ch )
2 mtand.2 . . 3  |-  ( (
ph  /\  ps )  ->  ch )
32ex 424 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41, 3mtod 170 1  |-  ( ph  ->  -.  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 359
This theorem is referenced by:  peano5  4809  sdomnsym  7169  unxpdomlem2  7251  cnfcom2lem  7592  cflim2  8077  fin23lem39  8164  isf32lem2  8168  konigthlem  8377  pythagtriplem4  13121  pythagtriplem11  13127  pythagtriplem13  13129  prmreclem1  13212  sylow1lem3  15162  efgredlema  15300  efgredlemc  15305  lssvancl1  15949  lspexchn1  16130  lspindp1  16133  zlpirlem3  16694  reconnlem2  18730  evlslem3  19803  aaliou2  20125  logdmnrp  20400  pntpbnd1  21148  ostth2lem4  21198  lmdvg  24143  ballotlemfcc  24531  ballotlemi1  24540  ballotlemii  24541  dmgmaddnn0  24591  wfrlem16  25296  nocvxminlem  25369  fphpd  26569  fiphp3d  26572  pellexlem6  26589  elpell1qr2  26627  pellqrex  26634  pellfund14gap  26642  unxpwdom3  26926  psgnunilem5  27087  stirlinglem5  27496  lcvnbtwn  29141  ncvr1  29388  lnnat  29542  lplncvrlvol  29731  dalem39  29826  lhpocnle  30131  cdleme17b  30402  cdlemg31c  30814  lclkrlem2o  31637  lcfrlem19  31677  baerlem5amN  31832  baerlem5bmN  31833  baerlem5abmN  31834  mapdh8ab  31893  mapdh8ad  31895  mapdh8c  31897
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator