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  2513  dfmoeu  2563  elALT2  5336  el  5411  fpropnf1  7297  findcard2d  9213  cantnflem1  9720  ttrclss  9751  ackbij1lem16  10342  fin1a2lem10  10517  inar1  10890  grur1a  10934  sqrt2irr  16449  lcmf  16840  lcmfunsnlem  16848  exprmfct  16912  pockthg  17116  prmgaplem5  17265  prmgaplem6  17266  drsdirfi  18511  obslbs  22069  mdetunilem9  22968  matunitlindflem1  23027  iscnp4  23614  isreg2  23728  dfconn2  23770  1stccnp  23814  flftg  24348  cnpfcf  24393  tsmsxp  24507  nmoleub  25083  vitalilem2  25963  vitalilem5  25966  c1lip1  26350  aalioulem6  26697  jensen  27349  2sqlem6  27783  dchrisumlem3  27851  pntlem3  27969  finsumvtxdg2sstep  30163  dfufd2lem  34165  bnj849  35638  cvmlift2lem1  36247  cvmlift2lem12  36259  mclsax  36514  nn0prpwlem  37301  axtco1from2  37454  mh-setindnd  37516  poimirlem30  38773  mapdordlem2  42897  eu6w  43891  iccelpart  48730  ichreuopeq  48770  sbgoldbalt  49094  sbgoldbm  49097  evengpop3  49111  evengpoap3  49112  bgoldbtbnd  49122  lindslinindsimp1  49784  iscnrm3r  50277  iscnrm3l  50280