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

Theorem mpid 40
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 24 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 mpid.2 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
42, 3mpdd 39 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  mp2d  44  pm2.43a  48  embantd  53  mtord  643  mpan2d  657  ceqsalt  2980  rspcimdv  3055  peano5  4870  riotass2  6579  oeordi  6832  isf34lem4  8259  domtriomlem  8324  axcclem  8339  rlimcn1  12384  climcn1  12387  climcn2  12388  dvdsgcd  13045  nprm  13095  pcqmul  13229  lubun  14552  grpid  14842  gexdvds  15220  uniopn  16972  tgcmp  17466  uncmp  17468  nconsubb  17488  kgencn2  17591  kqfvima  17764  isufil2  17942  cfinufil  17962  fin1aufil  17966  flimopn  18009  cnpflf  18035  flimfnfcls  18062  fcfnei  18069  metcnp3  18572  cncfco  18939  ellimc3  19768  dvfsumrlim  19917  cxploglim  20818  constr3trllem2  21640  grpoid  21813  blocnilem  22307  htthlem  22422  nmcexi  23531  dmdbr3  23810  dmdbr4  23811  atom1d  23858  dfon2lem8  25419  nn0prpwlem  26327  nn0prpw  26328  comppfsc  26389  filbcmb  26444  divrngidl  26640  psgnunilem4  27399  frgrancvvdeqlemB  28489  lubunNEW  29833  lshpcmp  29848  lsat0cv  29893  atnle  30177  lpolconN  32347
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator