Theorem mpid 44

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

Step	Hyp	Ref	Expression
1		mpid.1	. . 3 |- ( ph -> ch )
2	1	a1d 25	. 2 |- ( ph -> ( ps -> ch ) )
3		mpid.2	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
4	2, 3	mpdd 43	1 |- ( ph -> ( ps -> th ) )

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  49  pm2.43a  54  embantd  59  mtord  692  mpan2d  710  ceqsalt  3228  rspcimdv  3310  riotass2  6638  peano5  7089  oeordi  7667  isf34lem4  9199  domtriomlem  9264  axcclem  9279  ssnn0fi  12784  repswrevw  13533  rlimcn1  14319  climcn1  14322  climcn2  14323  dvdsgcd  15261  lcmfunsnlem2lem1  15351  coprmgcdb  15362  nprm  15401  pcqmul  15558  prmgaplem7  15761  lubun  17123  grpid  17457  psgnunilem4  17917  gexdvds  17999  scmate  20316  cayleyhamilton1  20697  uniopn  20702  tgcmp  21204  uncmp  21206  nconnsubb  21226  comppfsc  21335  kgencn2  21360  isufil2  21712  cfinufil  21732  fin1aufil  21736  flimopn  21779  cnpflf  21805  flimfnfcls  21832  fcfnei  21839  metcnp3  22345  cncfco  22710  ellimc3  23643  dvfsumrlim  23794  cxploglim  24704  nbuhgr2vtx1edgblem  26247  nbusgrvtxm1  26281  wlkp1lem6  26575  pthdlem2lem  26663  crctcshwlkn0lem4  26705  crctcshwlkn0lem5  26706  wwlks2onv  26847  eupth2  27099  frgrncvvdeqlem8  27170  grpoid  27374  blocnilem  27659  htthlem  27774  nmcexi  28885  dmdbr3  29164  dmdbr4  29165  atom1d  29212  mclsax  31466  dfon2lem8  31695  nn0prpwlem  32317  nn0prpw  32318  bj-ceqsalt0  32873  bj-ceqsalt1  32874  filbcmb  33535  divrngidl  33827  lshpcmp  34275  lsat0cv  34320  atnle  34604  lpolconN  36776  ss2iundf  37951  iccpartdisj  41373  lighneallem2  41523  lighneallem3  41524  lighneallem4  41527  proththd  41531  sgoldbeven3prm  41671  bgoldbtbndlem2  41694  upgrwlkupwlk  41721  lindslinindsimp1  42246  nn0sumshdiglemA  42413  setrec1lem4  42437