Theorem embantd 54

Description: Deduction embedding an antecedent. (Contributed by Wolf Lammen, 4-Oct-2013.)

Hypotheses

Ref	Expression
embantd.1	|- ( ph -> ps )
embantd.2	|- ( ph -> ( ch -> th ) )

Assertion

Ref	Expression
embantd	|- ( ph -> ( ( ps -> ch ) -> th ) )

Proof of Theorem embantd

Step	Hyp	Ref	Expression
1		embantd.1	. 2 |- ( ph -> ps )
2		embantd.2	. . 3 |- ( ph -> ( ch -> th ) )
3	2	imim2d 52	. 2 |- ( ph -> ( ( ps -> ch ) -> ( ps -> th ) ) )
4	1, 3	mpid 41	1 |- ( ph -> ( ( ps -> ch ) -> 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:  a2and  809  mo2v  2282  mo2vOLD  2283  mo2vOLDOLD  2284  el  4629  findcard2d  7763  cantnflem1  8109  cantnflem1OLD  8132  ackbij1lem16  8616  fin1a2lem10  8790  inar1  9154  grur1a  9198  sqrt2irr  13846  exprmfct  14113  pockthg  14286  drsdirfi  15428  obslbs  18568  mdetunilem9  18929  iscnp4  19570  isreg2  19684  dfcon2  19726  1stccnp  19769  flftg  20324  cnpfcf  20369  tsmsxp  20484  nmoleub  21065  vitalilem2  21845  vitalilem5  21848  c1lip1  22225  aalioulem6  22559  jensen  23143  2sqlem6  23469  dchrisumlem3  23501  pntlem3  23619  cvmlift2lem1  28498  cvmlift2lem12  28510  mclsax  28680  nn0prpwlem  29993  lindslinindsimp1  32356  bnj849  33279  bj-el  33680  mapdordlem2  36651