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

Theorem mpid 39
Description: A nested modus ponens deduction. (Contributed by NM, 14-Dec-2004.)
Hypotheses
Ref Expression
mpid.1  |-  ( ph  ->  ch )
mpid.2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Assertion
Ref Expression
mpid  |-  ( ph  ->  ( ps  ->  th )
)

Proof of Theorem mpid
StepHypRef Expression
1 mpid.1 . . 3  |-  ( ph  ->  ch )
21a1d 25 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 mpid.2 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
42, 3mpdd 38 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  mp2d  43  pm2.43a  48  embantd  53  mtord  658  mpan2d  672  ceqsalt  3082  rspcimdv  3161  riotass2  6266  peano5  6707  oeordi  7273  isf34lem4  8789  domtriomlem  8854  axcclem  8869  ssnn0fi  12135  repswrevw  12814  rlimcn1  13560  climcn1  13563  climcn2  13564  dvdsgcd  14390  nprm  14440  pcqmul  14586  lubun  16077  grpid  16409  psgnunilem4  16846  gexdvds  16928  scmate  19304  cayleyhamilton1  19685  uniopn  19698  tgcmp  20194  uncmp  20196  nconsubb  20216  comppfsc  20325  kgencn2  20350  isufil2  20701  cfinufil  20721  fin1aufil  20725  flimopn  20768  cnpflf  20794  flimfnfcls  20821  fcfnei  20828  metcnp3  21335  cncfco  21703  ellimc3  22575  dvfsumrlim  22724  cxploglim  23633  constr3trllem2  25068  frgrancvvdeqlemB  25455  grpoid  25639  blocnilem  26133  htthlem  26248  nmcexi  27358  dmdbr3  27637  dmdbr4  27638  atom1d  27685  mclsax  29781  dfon2lem8  30009  nn0prpwlem  30550  nn0prpw  30551  bj-ceqsalt0  31013  bj-ceqsalt1  31014  filbcmb  31513  divrngidl  31707  lshpcmp  32006  lsat0cv  32051  atnle  32335  lpolconN  34507  ss2iundf  35638  iccpartgt  37694  iccpartdisj  37704  bgoldbtbndlem2  37854  proththd  37860  lindslinindsimp1  38569  nn0sumshdiglemA  38750
  Copyright terms: Public domain W3C validator