MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mtand Structured version   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  4860  sdomnsym  7224  unxpdomlem2  7306  cnfcom2lem  7650  cflim2  8135  fin23lem39  8222  isf32lem2  8226  konigthlem  8435  pythagtriplem4  13185  pythagtriplem11  13191  pythagtriplem13  13193  prmreclem1  13276  sylow1lem3  15226  efgredlema  15364  efgredlemc  15369  lssvancl1  16013  lspexchn1  16194  lspindp1  16197  zlpirlem3  16762  reconnlem2  18850  evlslem3  19927  aaliou2  20249  logdmnrp  20524  pntpbnd1  21272  ostth2lem4  21322  lmdvg  24330  ballotlemfcc  24743  ballotlemi1  24752  ballotlemii  24753  dmgmaddnn0  24803  wfrlem16  25545  nocvxminlem  25637  mblfinlem  26234  fphpd  26868  fiphp3d  26871  pellexlem6  26888  elpell1qr2  26926  pellqrex  26933  pellfund14gap  26941  unxpwdom3  27224  psgnunilem5  27385  stirlinglem5  27794  lcvnbtwn  29760  ncvr1  30007  lnnat  30161  lplncvrlvol  30350  dalem39  30445  lhpocnle  30750  cdleme17b  31021  cdlemg31c  31433  lclkrlem2o  32256  lcfrlem19  32296  baerlem5amN  32451  baerlem5bmN  32452  baerlem5abmN  32453  mapdh8ab  32512  mapdh8ad  32514  mapdh8c  32516
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