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  2475  dfmoeu  2525  disj  4443  elALT2  5363  fpropnf1  7271  findcard2d  9182  cantnflem1  9704  ttrclss  9735  ackbij1lem16  10250  fin1a2lem10  10424  inar1  10790  grur1a  10834  sqrt2irr  16217  lcmf  16595  lcmfunsnlem  16603  exprmfct  16666  pockthg  16866  prmgaplem5  17015  prmgaplem6  17016  drsdirfi  18288  obslbs  21651  mdetunilem9  22509  iscnp4  23154  isreg2  23268  dfconn2  23310  1stccnp  23353  flftg  23887  cnpfcf  23932  tsmsxp  24046  nmoleub  24635  vitalilem2  25525  vitalilem5  25528  c1lip1  25917  aalioulem6  26259  jensen  26908  2sqlem6  27343  dchrisumlem3  27411  pntlem3  27529  finsumvtxdg2sstep  29350  bnj849  34492  cvmlift2lem1  34848  cvmlift2lem12  34860  mclsax  35115  nn0prpwlem  35742  matunitlindflem1  37024  poimirlem30  37058  mapdordlem2  41047  iccelpart  46696  ichreuopeq  46736  sbgoldbalt  47044  sbgoldbm  47047  evengpop3  47061  evengpoap3  47062  bgoldbtbnd  47072  lindslinindsimp1  47448  iscnrm3r  47890  iscnrm3l  47893