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  2483  dfmoeu  2534  disj  4387  elALT2  5301  fpropnf1  7172  findcard2d  8987  cantnflem1  9491  ttrclss  9522  ackbij1lem16  10037  fin1a2lem10  10211  inar1  10577  grur1a  10621  sqrt2irr  16003  lcmf  16383  lcmfunsnlem  16391  exprmfct  16454  pockthg  16652  prmgaplem5  16801  prmgaplem6  16802  drsdirfi  18068  obslbs  20982  mdetunilem9  21814  iscnp4  22459  isreg2  22573  dfconn2  22615  1stccnp  22658  flftg  23192  cnpfcf  23237  tsmsxp  23351  nmoleub  23940  vitalilem2  24818  vitalilem5  24821  c1lip1  25206  aalioulem6  25542  jensen  26183  2sqlem6  26616  dchrisumlem3  26684  pntlem3  26802  finsumvtxdg2sstep  27961  bnj849  32950  cvmlift2lem1  33309  cvmlift2lem12  33321  mclsax  33576  nn0prpwlem  34556  matunitlindflem1  35817  poimirlem30  35851  mapdordlem2  39693  iccelpart  44943  ichreuopeq  44983  sbgoldbalt  45291  sbgoldbm  45294  evengpop3  45308  evengpoap3  45309  bgoldbtbnd  45319  lindslinindsimp1  45856  iscnrm3r  46300  iscnrm3l  46303