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  4447  elALT2  5367  fpropnf1  7268  findcard2d  9168  cantnflem1  9686  ttrclss  9717  ackbij1lem16  10232  fin1a2lem10  10406  inar1  10772  grur1a  10816  sqrt2irr  16196  lcmf  16574  lcmfunsnlem  16582  exprmfct  16645  pockthg  16843  prmgaplem5  16992  prmgaplem6  16993  drsdirfi  18262  obslbs  21504  mdetunilem9  22342  iscnp4  22987  isreg2  23101  dfconn2  23143  1stccnp  23186  flftg  23720  cnpfcf  23765  tsmsxp  23879  nmoleub  24468  vitalilem2  25350  vitalilem5  25353  c1lip1  25738  aalioulem6  26074  jensen  26717  2sqlem6  27150  dchrisumlem3  27218  pntlem3  27336  finsumvtxdg2sstep  29061  bnj849  34222  cvmlift2lem1  34579  cvmlift2lem12  34591  mclsax  34846  nn0prpwlem  35510  matunitlindflem1  36787  poimirlem30  36821  mapdordlem2  40811  iccelpart  46400  ichreuopeq  46440  sbgoldbalt  46748  sbgoldbm  46751  evengpop3  46765  evengpoap3  46766  bgoldbtbnd  46776  lindslinindsimp1  47226  iscnrm3r  47669  iscnrm3l  47672