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  2810  rspcimdv  2885  peano5  4679  riotass2  6332  oeordi  6585  isf34lem4  8003  domtriomlem  8068  axcclem  8083  rlimcn1  12062  climcn1  12065  climcn2  12066  dvdsgcd  12722  nprm  12772  pcqmul  12906  lubun  14227  grpid  14517  gexdvds  14895  uniopn  16643  tgcmp  17128  uncmp  17130  nconsubb  17149  kgencn2  17252  kqfvima  17421  isufil2  17603  cfinufil  17623  fin1aufil  17627  flimopn  17670  cnpflf  17696  flimfnfcls  17723  fcfnei  17730  metcnp3  18086  cncfco  18411  ellimc3  19229  dvfsumrlim  19378  cxploglim  20272  grpoid  20890  blocnilem  21382  htthlem  21497  nmcexi  22606  dmdbr3  22885  dmdbr4  22886  atom1d  22933  dfon2lem8  24146  wl-adnestantdALTOLD  24909  grpodivone  25373  grpodivfo  25374  osneisi  25531  bsstrs  26146  nbssntrs  26147  nn0prpwlem  26238  nn0prpw  26239  comppfsc  26307  filbcmb  26432  divrngidl  26653  psgnunilem4  27420  lubunNEW  29163  lshpcmp  29178  lsat0cv  29223  atnle  29507  lpolconN  31677
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator