Theorem embantd 59

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

Hypotheses

Ref	Expression
embantd.1	⊢ (𝜑 → 𝜓)
embantd.2	⊢ (𝜑 → (𝜒 → 𝜃))

Assertion

Ref	Expression
embantd	⊢ (𝜑 → ((𝜓 → 𝜒) → 𝜃))

Proof of Theorem embantd

Step	Hyp	Ref	Expression
1		embantd.1	. 2 ⊢ (𝜑 → 𝜓)
2		embantd.2	. . 3 ⊢ (𝜑 → (𝜒 → 𝜃))
3	2	imim2d 57	. 2 ⊢ (𝜑 → ((𝜓 → 𝜒) → (𝜓 → 𝜃)))
4	1, 3	mpid 44	1 ⊢ (𝜑 → ((𝜓 → 𝜒) → 𝜃))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  dfsb1  2510  dfmoeu  2618  el  5272  fpropnf1  7027  findcard2d  8762  cantnflem1  9154  ackbij1lem16  9659  fin1a2lem10  9833  inar1  10199  grur1a  10243  sqrt2irr  15604  lcmf  15979  lcmfunsnlem  15987  exprmfct  16050  pockthg  16244  prmgaplem5  16393  prmgaplem6  16394  drsdirfi  17550  obslbs  20876  mdetunilem9  21231  iscnp4  21873  isreg2  21987  dfconn2  22029  1stccnp  22072  flftg  22606  cnpfcf  22651  tsmsxp  22765  nmoleub  23342  vitalilem2  24212  vitalilem5  24215  c1lip1  24596  aalioulem6  24928  jensen  25568  2sqlem6  26001  dchrisumlem3  26069  pntlem3  26187  finsumvtxdg2sstep  27333  bnj849  32199  cvmlift2lem1  32551  cvmlift2lem12  32563  mclsax  32818  nn0prpwlem  33672  matunitlindflem1  34890  poimirlem30  34924  mapdordlem2  38775  iccelpart  43600  ichreuopeq  43642  sbgoldbalt  43953  sbgoldbm  43956  evengpop3  43970  evengpoap3  43971  bgoldbtbnd  43981  lindslinindsimp1  44519