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  2474  dfmoeu  2524  disj  4448  elALT2  5368  fpropnf1  7275  findcard2d  9189  cantnflem1  9712  ttrclss  9743  ackbij1lem16  10258  fin1a2lem10  10432  inar1  10798  grur1a  10842  sqrt2irr  16225  lcmf  16603  lcmfunsnlem  16611  exprmfct  16674  pockthg  16874  prmgaplem5  17023  prmgaplem6  17024  drsdirfi  18296  obslbs  21668  mdetunilem9  22552  iscnp4  23197  isreg2  23311  dfconn2  23353  1stccnp  23396  flftg  23930  cnpfcf  23975  tsmsxp  24089  nmoleub  24678  vitalilem2  25568  vitalilem5  25571  c1lip1  25960  aalioulem6  26302  jensen  26951  2sqlem6  27386  dchrisumlem3  27454  pntlem3  27572  finsumvtxdg2sstep  29419  bnj849  34626  cvmlift2lem1  34982  cvmlift2lem12  34994  mclsax  35249  nn0prpwlem  35876  matunitlindflem1  37159  poimirlem30  37193  mapdordlem2  41179  iccelpart  46836  ichreuopeq  46876  sbgoldbalt  47184  sbgoldbm  47187  evengpop3  47201  evengpoap3  47202  bgoldbtbnd  47212  lindslinindsimp1  47637  iscnrm3r  48079  iscnrm3l  48082