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  2480  dfmoeu  2530  disj  4446  elALT2  5366  fpropnf1  7262  findcard2d  9162  cantnflem1  9680  ttrclss  9711  ackbij1lem16  10226  fin1a2lem10  10400  inar1  10766  grur1a  10810  sqrt2irr  16188  lcmf  16566  lcmfunsnlem  16574  exprmfct  16637  pockthg  16835  prmgaplem5  16984  prmgaplem6  16985  drsdirfi  18254  obslbs  21276  mdetunilem9  22113  iscnp4  22758  isreg2  22872  dfconn2  22914  1stccnp  22957  flftg  23491  cnpfcf  23536  tsmsxp  23650  nmoleub  24239  vitalilem2  25117  vitalilem5  25120  c1lip1  25505  aalioulem6  25841  jensen  26482  2sqlem6  26915  dchrisumlem3  26983  pntlem3  27101  finsumvtxdg2sstep  28795  bnj849  33924  cvmlift2lem1  34281  cvmlift2lem12  34293  mclsax  34548  nn0prpwlem  35195  matunitlindflem1  36472  poimirlem30  36506  mapdordlem2  40496  iccelpart  46087  ichreuopeq  46127  sbgoldbalt  46435  sbgoldbm  46438  evengpop3  46452  evengpoap3  46453  bgoldbtbnd  46463  lindslinindsimp1  47091  iscnrm3r  47534  iscnrm3l  47537