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  3007  rspcimdv  3086  riotass2  6091  peano5  6511  oeordi  7038  isf34lem4  8558  domtriomlem  8623  axcclem  8638  repswrevw  12436  rlimcn1  13078  climcn1  13081  climcn2  13082  dvdsgcd  13739  nprm  13789  pcqmul  13932  lubun  15305  grpid  15585  psgnunilem4  16015  gexdvds  16095  uniopn  18522  tgcmp  19016  uncmp  19018  nconsubb  19039  kgencn2  19142  kqfvima  19315  isufil2  19493  cfinufil  19513  fin1aufil  19517  flimopn  19560  cnpflf  19586  flimfnfcls  19613  fcfnei  19620  metcnp3  20127  cncfco  20495  ellimc3  21366  dvfsumrlim  21515  cxploglim  22383  constr3trllem2  23549  grpoid  23722  blocnilem  24216  htthlem  24331  nmcexi  25442  dmdbr3  25721  dmdbr4  25722  atom1d  25769  dfon2lem8  27615  nn0prpwlem  28529  nn0prpw  28530  comppfsc  28591  filbcmb  28646  divrngidl  28840  frgrancvvdeqlemB  30643  ssnn0fi  30758  lindslinindsimp1  31003  bj-ceqsalt0  32396  bj-ceqsalt1  32397  lshpcmp  32645  lsat0cv  32690  atnle  32974  lpolconN  35144
  Copyright terms: Public domain W3C validator