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  4679  sdomnsym  6986  unxpdomlem2  7068  cnfcom2lem  7404  cflim2  7889  fin23lem39  7976  isf32lem2  7980  konigthlem  8190  pythagtriplem4  12872  pythagtriplem11  12878  pythagtriplem13  12880  prmreclem1  12963  sylow1lem3  14911  efgredlema  15049  efgredlemc  15054  lssvancl1  15702  lspexchn1  15883  lspindp1  15886  zlpirlem3  16443  reconnlem2  18332  evlslem3  19398  aaliou2  19720  logdmnrp  19988  pntpbnd1  20735  ostth2lem4  20785  lmdvg  23376  wfrlem16  24271  nocvxminlem  24344  fphpd  26899  fiphp3d  26902  pellexlem6  26919  elpell1qr2  26957  pellqrex  26964  pellfund14gap  26972  unxpwdom3  27256  psgnunilem5  27417  stirlinglem5  27827  lcvnbtwn  29215  ncvr1  29462  lnnat  29616  lplncvrlvol  29805  dalem39  29900  lhpocnle  30205  cdleme17b  30476  cdlemg31c  30888  lclkrlem2o  31711  lcfrlem19  31751  baerlem5amN  31906  baerlem5bmN  31907  baerlem5abmN  31908  mapdh8ab  31967  mapdh8ad  31969  mapdh8c  31971
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