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  2273  mo2vOLD  2274  mo2vOLDOLD  2275  el  4615  findcard2d  7760  cantnflem1  8106  cantnflem1OLD  8129  ackbij1lem16  8613  fin1a2lem10  8787  inar1  9151  grur1a  9195  sqrt2irr  13854  exprmfct  14123  pockthg  14296  drsdirfi  15436  obslbs  18628  mdetunilem9  18989  iscnp4  19630  isreg2  19744  dfcon2  19786  1stccnp  19829  flftg  20363  cnpfcf  20408  tsmsxp  20523  nmoleub  21104  vitalilem2  21884  vitalilem5  21887  c1lip1  22264  aalioulem6  22598  jensen  23183  2sqlem6  23509  dchrisumlem3  23541  pntlem3  23659  cvmlift2lem1  28613  cvmlift2lem12  28625  mclsax  28795  nn0prpwlem  30108  lindslinindsimp1  32768  bnj849  33690  bj-el  34094  mapdordlem2  37066