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  2533  elALT2  5309  fpropnf1  7207  findcard2d  9083  cantnflem1  9586  ttrclss  9617  ackbij1lem16  10132  fin1a2lem10  10307  inar1  10673  grur1a  10717  sqrt2irr  16160  lcmf  16546  lcmfunsnlem  16554  exprmfct  16617  pockthg  16820  prmgaplem5  16969  prmgaplem6  16970  drsdirfi  18213  obslbs  21669  mdetunilem9  22536  iscnp4  23179  isreg2  23293  dfconn2  23335  1stccnp  23378  flftg  23912  cnpfcf  23957  tsmsxp  24071  nmoleub  24647  vitalilem2  25538  vitalilem5  25541  c1lip1  25930  aalioulem6  26273  jensen  26927  2sqlem6  27362  dchrisumlem3  27430  pntlem3  27548  finsumvtxdg2sstep  29530  dfufd2lem  33521  bnj849  34958  cvmlift2lem1  35367  cvmlift2lem12  35379  mclsax  35634  nn0prpwlem  36387  matunitlindflem1  37676  poimirlem30  37710  mapdordlem2  41756  eu6w  42794  iccelpart  47557  ichreuopeq  47597  sbgoldbalt  47905  sbgoldbm  47908  evengpop3  47922  evengpoap3  47923  bgoldbtbnd  47933  lindslinindsimp1  48582  iscnrm3r  49072  iscnrm3l  49075