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

Theorem mtand 640
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 423 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41, 3mtod 168 1  |-  ( ph  ->  -.  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 358
This theorem is referenced by:  peano5  4695  sdomnsym  7002  unxpdomlem2  7084  cnfcom2lem  7420  cflim2  7905  fin23lem39  7992  isf32lem2  7996  konigthlem  8206  pythagtriplem4  12888  pythagtriplem11  12894  pythagtriplem13  12896  prmreclem1  12979  sylow1lem3  14927  efgredlema  15065  efgredlemc  15070  lssvancl1  15718  lspexchn1  15899  lspindp1  15902  zlpirlem3  16459  reconnlem2  18348  evlslem3  19414  aaliou2  19736  logdmnrp  20004  pntpbnd1  20751  ostth2lem4  20801  lmdvg  23391  wfrlem16  24342  nocvxminlem  24415  fphpd  27002  fiphp3d  27005  pellexlem6  27022  elpell1qr2  27060  pellqrex  27067  pellfund14gap  27075  unxpwdom3  27359  psgnunilem5  27520  stirlinglem5  27930  lcvnbtwn  29837  ncvr1  30084  lnnat  30238  lplncvrlvol  30427  dalem39  30522  lhpocnle  30827  cdleme17b  31098  cdlemg31c  31510  lclkrlem2o  32333  lcfrlem19  32373  baerlem5amN  32528  baerlem5bmN  32529  baerlem5abmN  32530  mapdh8ab  32589  mapdh8ad  32591  mapdh8c  32593
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 177  df-an 360
  Copyright terms: Public domain W3C validator