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

Theorem mpid 41
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 40 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  45  pm2.43a  49  embantd  54  mtord  660  mpan2d  674  ceqsalt  3118  rspcimdv  3197  riotass2  6269  peano5  6708  oeordi  7238  isf34lem4  8760  domtriomlem  8825  axcclem  8840  ssnn0fi  12073  repswrevw  12737  rlimcn1  13390  climcn1  13393  climcn2  13394  dvdsgcd  14058  nprm  14108  pcqmul  14254  lubun  15627  grpid  15959  psgnunilem4  16396  gexdvds  16478  scmate  18885  cayleyhamilton1  19266  uniopn  19279  tgcmp  19774  uncmp  19776  nconsubb  19797  comppfsc  19906  kgencn2  19931  isufil2  20282  cfinufil  20302  fin1aufil  20306  flimopn  20349  cnpflf  20375  flimfnfcls  20402  fcfnei  20409  metcnp3  20916  cncfco  21284  ellimc3  22156  dvfsumrlim  22305  cxploglim  23179  constr3trllem2  24523  frgrancvvdeqlemB  24910  grpoid  25097  blocnilem  25591  htthlem  25706  nmcexi  26817  dmdbr3  27096  dmdbr4  27097  atom1d  27144  mclsax  28802  dfon2lem8  29197  nn0prpwlem  30115  nn0prpw  30116  filbcmb  30206  divrngidl  30400  lindslinindsimp1  32793  bj-ceqsalt0  34197  bj-ceqsalt1  34198  lshpcmp  34453  lsat0cv  34498  atnle  34782  lpolconN  36954
  Copyright terms: Public domain W3C validator