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

Theorem mpid 42
Description: A nested modus ponens deduction. Deduction associated with mpi 20. (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 26 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 mpid.2 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
42, 3mpdd 41 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  46  pm2.43a  51  embantd  56  mtord  664  mpan2d  678  ceqsalt  3041  rspcimdv  3121  riotass2  6232  peano5  6669  oeordi  7238  isf34lem4  8753  domtriomlem  8818  axcclem  8833  ssnn0fi  12142  repswrevw  12830  rlimcn1  13590  climcn1  13593  climcn2  13594  dvdsgcd  14449  lcmfunsnlem2lem1  14549  nprm  14576  coprmgcdb  14592  pcqmul  14741  prmgaplem7  14965  lubun  16307  grpid  16639  psgnunilem4  17076  gexdvds  17173  scmate  19472  cayleyhamilton1  19853  uniopn  19864  tgcmp  20353  uncmp  20355  nconsubb  20375  comppfsc  20484  kgencn2  20509  isufil2  20860  cfinufil  20880  fin1aufil  20884  flimopn  20927  cnpflf  20953  flimfnfcls  20980  fcfnei  20987  metcnp3  21492  cncfco  21876  ellimc3  22771  dvfsumrlim  22920  cxploglim  23840  constr3trllem2  25316  frgrancvvdeqlemB  25703  grpoid  25888  blocnilem  26382  htthlem  26507  nmcexi  27616  dmdbr3  27895  dmdbr4  27896  atom1d  27943  mclsax  30154  dfon2lem8  30382  nn0prpwlem  30922  nn0prpw  30923  bj-ceqsalt0  31393  bj-ceqsalt1  31394  filbcmb  31974  divrngidl  32168  lshpcmp  32466  lsat0cv  32511  atnle  32795  lpolconN  34967  ss2iundf  36164  iccpartgt  38554  iccpartdisj  38564  bgoldbtbndlem2  38714  proththd  38727  nbuhgr2vtx1edgblem  39155  lindslinindsimp1  39843  nn0sumshdiglemA  40023
  Copyright terms: Public domain W3C validator