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  2499  dfmoeu  2553  disj  4344  el  5238  fpropnf1  7017  findcard2d  8737  cantnflem1  9185  ackbij1lem16  9695  fin1a2lem10  9869  inar1  10235  grur1a  10279  sqrt2irr  15650  lcmf  16029  lcmfunsnlem  16037  exprmfct  16100  pockthg  16297  prmgaplem5  16446  prmgaplem6  16447  drsdirfi  17614  obslbs  20495  mdetunilem9  21320  iscnp4  21963  isreg2  22077  dfconn2  22119  1stccnp  22162  flftg  22696  cnpfcf  22741  tsmsxp  22855  nmoleub  23433  vitalilem2  24309  vitalilem5  24312  c1lip1  24696  aalioulem6  25032  jensen  25673  2sqlem6  26106  dchrisumlem3  26174  pntlem3  26292  finsumvtxdg2sstep  27438  bnj849  32425  cvmlift2lem1  32780  cvmlift2lem12  32792  mclsax  33047  nn0prpwlem  34060  matunitlindflem1  35333  poimirlem30  35367  mapdordlem2  39213  iccelpart  44318  ichreuopeq  44358  sbgoldbalt  44666  sbgoldbm  44669  evengpop3  44683  evengpoap3  44684  bgoldbtbnd  44694  lindslinindsimp1  45231