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  2479  dfmoeu  2529  disj  4403  elALT2  5311  fpropnf1  7208  findcard2d  9090  cantnflem1  9604  ttrclss  9635  ackbij1lem16  10147  fin1a2lem10  10322  inar1  10688  grur1a  10732  sqrt2irr  16176  lcmf  16562  lcmfunsnlem  16570  exprmfct  16633  pockthg  16836  prmgaplem5  16985  prmgaplem6  16986  drsdirfi  18229  obslbs  21655  mdetunilem9  22523  iscnp4  23166  isreg2  23280  dfconn2  23322  1stccnp  23365  flftg  23899  cnpfcf  23944  tsmsxp  24058  nmoleub  24635  vitalilem2  25526  vitalilem5  25529  c1lip1  25918  aalioulem6  26261  jensen  26915  2sqlem6  27350  dchrisumlem3  27418  pntlem3  27536  finsumvtxdg2sstep  29513  dfufd2lem  33496  bnj849  34891  cvmlift2lem1  35274  cvmlift2lem12  35286  mclsax  35541  nn0prpwlem  36295  matunitlindflem1  37595  poimirlem30  37629  mapdordlem2  41616  eu6w  42649  iccelpart  47418  ichreuopeq  47458  sbgoldbalt  47766  sbgoldbm  47769  evengpop3  47783  evengpoap3  47784  bgoldbtbnd  47794  lindslinindsimp1  48443  iscnrm3r  48933  iscnrm3l  48936