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

Theorem mpid 37
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 22 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 mpid.2 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
42, 3mpdd 36 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  mp2d  41  pm2.43a  45  embantd  50  mtord  641  mpan2d  655  ceqsalt  2823  rspcimdv  2898  peano5  4695  riotass2  6348  oeordi  6601  isf34lem4  8019  domtriomlem  8084  axcclem  8099  rlimcn1  12078  climcn1  12081  climcn2  12082  dvdsgcd  12738  nprm  12788  pcqmul  12922  lubun  14243  grpid  14533  gexdvds  14911  uniopn  16659  tgcmp  17144  uncmp  17146  nconsubb  17165  kgencn2  17268  kqfvima  17437  isufil2  17619  cfinufil  17639  fin1aufil  17643  flimopn  17686  cnpflf  17712  flimfnfcls  17739  fcfnei  17746  metcnp3  18102  cncfco  18427  ellimc3  19245  dvfsumrlim  19394  cxploglim  20288  grpoid  20906  blocnilem  21398  htthlem  21513  nmcexi  22622  dmdbr3  22901  dmdbr4  22902  atom1d  22949  dfon2lem8  24217  wl-adnestantdALTOLD  24981  grpodivone  25476  grpodivfo  25477  osneisi  25634  bsstrs  26249  nbssntrs  26250  nn0prpwlem  26341  nn0prpw  26342  comppfsc  26410  filbcmb  26535  divrngidl  26756  psgnunilem4  27523  constr3trllem2  28397  lubunNEW  29785  lshpcmp  29800  lsat0cv  29845  atnle  30129  lpolconN  32299
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator