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  2485  dfmoeu  2535  elALT2  5314  fpropnf1  7213  findcard2d  9091  cantnflem1  9598  ttrclss  9629  ackbij1lem16  10144  fin1a2lem10  10319  inar1  10686  grur1a  10730  sqrt2irr  16174  lcmf  16560  lcmfunsnlem  16568  exprmfct  16631  pockthg  16834  prmgaplem5  16983  prmgaplem6  16984  drsdirfi  18228  obslbs  21685  mdetunilem9  22564  iscnp4  23207  isreg2  23321  dfconn2  23363  1stccnp  23406  flftg  23940  cnpfcf  23985  tsmsxp  24099  nmoleub  24675  vitalilem2  25566  vitalilem5  25569  c1lip1  25958  aalioulem6  26301  jensen  26955  2sqlem6  27390  dchrisumlem3  27458  pntlem3  27576  finsumvtxdg2sstep  29623  dfufd2lem  33630  bnj849  35081  cvmlift2lem1  35496  cvmlift2lem12  35508  mclsax  35763  nn0prpwlem  36516  mh-setindnd  36667  matunitlindflem1  37813  poimirlem30  37847  mapdordlem2  41893  eu6w  42915  iccelpart  47675  ichreuopeq  47715  sbgoldbalt  48023  sbgoldbm  48026  evengpop3  48040  evengpoap3  48041  bgoldbtbnd  48051  lindslinindsimp1  48699  iscnrm3r  49189  iscnrm3l  49192