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  3136  rspcimdv  3215  riotass2  6271  peano5  6702  oeordi  7236  isf34lem4  8756  domtriomlem  8821  axcclem  8836  ssnn0fi  12061  repswrevw  12720  rlimcn1  13373  climcn1  13376  climcn2  13377  dvdsgcd  14039  nprm  14089  pcqmul  14235  lubun  15609  grpid  15892  psgnunilem4  16325  gexdvds  16407  scmate  18795  cayleyhamilton1  19176  uniopn  19189  tgcmp  19683  uncmp  19685  nconsubb  19706  kgencn2  19809  kqfvima  19982  isufil2  20160  cfinufil  20180  fin1aufil  20184  flimopn  20227  cnpflf  20253  flimfnfcls  20280  fcfnei  20287  metcnp3  20794  cncfco  21162  ellimc3  22034  dvfsumrlim  22183  cxploglim  23051  constr3trllem2  24343  frgrancvvdeqlemB  24731  grpoid  24917  blocnilem  25411  htthlem  25526  nmcexi  26637  dmdbr3  26916  dmdbr4  26917  atom1d  26964  dfon2lem8  28815  nn0prpwlem  29733  nn0prpw  29734  comppfsc  29795  filbcmb  29850  divrngidl  30044  lindslinindsimp1  32148  bj-ceqsalt0  33539  bj-ceqsalt1  33540  lshpcmp  33794  lsat0cv  33839  atnle  34123  lpolconN  36293
  Copyright terms: Public domain W3C validator