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  2536  disj  4450  elALT2  5369  fpropnf1  7287  findcard2d  9206  cantnflem1  9729  ttrclss  9760  ackbij1lem16  10274  fin1a2lem10  10449  inar1  10815  grur1a  10859  sqrt2irr  16285  lcmf  16670  lcmfunsnlem  16678  exprmfct  16741  pockthg  16944  prmgaplem5  17093  prmgaplem6  17094  drsdirfi  18351  obslbs  21750  mdetunilem9  22626  iscnp4  23271  isreg2  23385  dfconn2  23427  1stccnp  23470  flftg  24004  cnpfcf  24049  tsmsxp  24163  nmoleub  24752  vitalilem2  25644  vitalilem5  25647  c1lip1  26036  aalioulem6  26379  jensen  27032  2sqlem6  27467  dchrisumlem3  27535  pntlem3  27653  finsumvtxdg2sstep  29567  dfufd2lem  33577  bnj849  34939  cvmlift2lem1  35307  cvmlift2lem12  35319  mclsax  35574  nn0prpwlem  36323  matunitlindflem1  37623  poimirlem30  37657  mapdordlem2  41639  eu6w  42686  iccelpart  47420  ichreuopeq  47460  sbgoldbalt  47768  sbgoldbm  47771  evengpop3  47785  evengpoap3  47786  bgoldbtbnd  47796  lindslinindsimp1  48374  iscnrm3r  48845  iscnrm3l  48848