Theorem embantd 60

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 58	. 2 ⊢ (𝜑 → ((𝜓 → 𝜒) → (𝜓 → 𝜃)))
4	1, 3	mpid 45	1 ⊢ (𝜑 → ((𝜓 → 𝜒) → 𝜃))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  dfsb1  2512  dfmoeu  2562  elALT2  5338  el  5417  fpropnf1  7268  findcard2d  9165  cantnflem1  9672  ttrclss  9703  ackbij1lem16  10240  fin1a2lem10  10415  inar1  10788  grur1a  10832  sqrt2irr  16343  lcmf  16729  lcmfunsnlem  16737  exprmfct  16801  pockthg  17004  prmgaplem5  17153  prmgaplem6  17154  drsdirfi  18399  obslbs  21949  mdetunilem9  22848  matunitlindflem1  22907  iscnp4  23494  isreg2  23608  dfconn2  23650  1stccnp  23694  flftg  24228  cnpfcf  24273  tsmsxp  24387  nmoleub  24963  vitalilem2  25843  vitalilem5  25846  c1lip1  26231  aalioulem6  26580  jensen  27233  2sqlem6  27667  dchrisumlem3  27735  pntlem3  27853  finsumvtxdg2sstep  30017  dfufd2lem  33967  bnj849  35442  cvmlift2lem1  35889  cvmlift2lem12  35901  mclsax  36156  nn0prpwlem  36949  axtco1from2  37102  mh-setindnd  37164  poimirlem30  38407  mapdordlem2  42518  eu6w  43530  iccelpart  48341  ichreuopeq  48381  sbgoldbalt  48705  sbgoldbm  48708  evengpop3  48722  evengpoap3  48723  bgoldbtbnd  48733  lindslinindsimp1  49395  iscnrm3r  49882  iscnrm3l  49885