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  2486  dfmoeu  2537  disj  4386  el  5295  fpropnf1  7134  findcard2d  8914  cantnflem1  9408  ttrclss  9439  ackbij1lem16  9975  fin1a2lem10  10149  inar1  10515  grur1a  10559  sqrt2irr  15939  lcmf  16319  lcmfunsnlem  16327  exprmfct  16390  pockthg  16588  prmgaplem5  16737  prmgaplem6  16738  drsdirfi  18004  obslbs  20918  mdetunilem9  21750  iscnp4  22395  isreg2  22509  dfconn2  22551  1stccnp  22594  flftg  23128  cnpfcf  23173  tsmsxp  23287  nmoleub  23876  vitalilem2  24754  vitalilem5  24757  c1lip1  25142  aalioulem6  25478  jensen  26119  2sqlem6  26552  dchrisumlem3  26620  pntlem3  26738  finsumvtxdg2sstep  27897  bnj849  32884  cvmlift2lem1  33243  cvmlift2lem12  33255  mclsax  33510  nn0prpwlem  34490  matunitlindflem1  35752  poimirlem30  35786  mapdordlem2  39630  iccelpart  44837  ichreuopeq  44877  sbgoldbalt  45185  sbgoldbm  45188  evengpop3  45202  evengpoap3  45203  bgoldbtbnd  45213  lindslinindsimp1  45750  iscnrm3r  46194  iscnrm3l  46197