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  2489  dfmoeu  2539  elALT2  5305  el  5384  fpropnf1  7218  findcard2d  9098  cantnflem1  9608  ttrclss  9639  ackbij1lem16  10154  fin1a2lem10  10329  inar1  10696  grur1a  10740  sqrt2irr  16214  lcmf  16600  lcmfunsnlem  16608  exprmfct  16672  pockthg  16875  prmgaplem5  17024  prmgaplem6  17025  drsdirfi  18269  obslbs  21712  mdetunilem9  22610  iscnp4  23253  isreg2  23367  dfconn2  23409  1stccnp  23452  flftg  23986  cnpfcf  24031  tsmsxp  24145  nmoleub  24721  vitalilem2  25601  vitalilem5  25604  c1lip1  25989  aalioulem6  26328  jensen  26977  2sqlem6  27411  dchrisumlem3  27479  pntlem3  27597  finsumvtxdg2sstep  29643  dfufd2lem  33639  bnj849  35114  cvmlift2lem1  35537  cvmlift2lem12  35549  mclsax  35804  nn0prpwlem  36557  axtco1from2  36710  mh-setindnd  36772  matunitlindflem1  37990  poimirlem30  38024  mapdordlem2  42136  eu6w  43133  iccelpart  47915  ichreuopeq  47955  sbgoldbalt  48279  sbgoldbm  48282  evengpop3  48296  evengpoap3  48297  bgoldbtbnd  48307  lindslinindsimp1  48955  iscnrm3r  49445  iscnrm3l  49448