Theorem embantd 59

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 57	. 2 |- ( ph -> ( ( ps -> ch ) -> ( ps -> th ) ) )
4	1, 3	mpid 44	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  853  mo2v  2477  el  4847  fpropnf1  6524  findcard2d  8202  cantnflem1  8586  ackbij1lem16  9057  fin1a2lem10  9231  inar1  9597  grur1a  9641  sqrt2irr  14979  lcmf  15346  lcmfunsnlem  15354  exprmfct  15416  pockthg  15610  prmgaplem5  15759  prmgaplem6  15760  drsdirfi  16938  obslbs  20074  mdetunilem9  20426  iscnp4  21067  isreg2  21181  dfconn2  21222  1stccnp  21265  flftg  21800  cnpfcf  21845  tsmsxp  21958  nmoleub  22535  vitalilem2  23378  vitalilem5  23381  c1lip1  23760  aalioulem6  24092  jensen  24715  2sqlem6  25148  dchrisumlem3  25180  pntlem3  25298  finsumvtxdg2sstep  26445  bnj849  30995  cvmlift2lem1  31284  cvmlift2lem12  31296  mclsax  31466  nn0prpwlem  32317  bj-el  32796  matunitlindflem1  33405  poimirlem30  33439  mapdordlem2  36926  iccelpart  41369  sbgoldbalt  41669  sbgoldbm  41672  evengpop3  41686  evengpoap3  41687  bgoldbtbnd  41697  lindslinindsimp1  42246