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:  mo2v  2269  mo2vOLD  2270  mo2vOLDOLD  2271  el  4585  findcard2d  7668  cantnflem1  8011  cantnflem1OLD  8034  ackbij1lem16  8518  fin1a2lem10  8692  inar1  9056  grur1a  9100  sqr2irr  13652  exprmfct  13917  pockthg  14088  drsdirfi  15230  obslbs  18283  mdetunilem9  18561  iscnp4  19002  isreg2  19116  dfcon2  19158  1stccnp  19201  flftg  19704  cnpfcf  19749  tsmsxp  19864  nmoleub  20445  vitalilem2  21225  vitalilem5  21228  c1lip1  21605  aalioulem6  21939  jensen  22518  2sqlem6  22844  dchrisumlem3  22876  pntlem3  22994  cvmlift2lem1  27355  cvmlift2lem12  27367  nn0prpwlem  28685  lindslinindsimp1  31143  bnj849  32270  bj-el  32669  mapdordlem2  35640