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  4413  elALT2  5324  fpropnf1  7242  findcard2d  9130  cantnflem1  9642  ttrclss  9673  ackbij1lem16  10187  fin1a2lem10  10362  inar1  10728  grur1a  10772  sqrt2irr  16217  lcmf  16603  lcmfunsnlem  16611  exprmfct  16674  pockthg  16877  prmgaplem5  17026  prmgaplem6  17027  drsdirfi  18266  obslbs  21639  mdetunilem9  22507  iscnp4  23150  isreg2  23264  dfconn2  23306  1stccnp  23349  flftg  23883  cnpfcf  23928  tsmsxp  24042  nmoleub  24619  vitalilem2  25510  vitalilem5  25513  c1lip1  25902  aalioulem6  26245  jensen  26899  2sqlem6  27334  dchrisumlem3  27402  pntlem3  27520  finsumvtxdg2sstep  29477  dfufd2lem  33520  bnj849  34915  cvmlift2lem1  35289  cvmlift2lem12  35301  mclsax  35556  nn0prpwlem  36310  matunitlindflem1  37610  poimirlem30  37644  mapdordlem2  41631  eu6w  42664  iccelpart  47434  ichreuopeq  47474  sbgoldbalt  47782  sbgoldbm  47785  evengpop3  47799  evengpoap3  47800  bgoldbtbnd  47810  lindslinindsimp1  48446  iscnrm3r  48936  iscnrm3l  48939