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:  a2and  852  mo2v  2476  el  4807  fpropnf1  6478  findcard2d  8146  cantnflem1  8530  ackbij1lem16  9001  fin1a2lem10  9175  inar1  9541  grur1a  9585  sqrt2irr  14903  lcmf  15270  lcmfunsnlem  15278  exprmfct  15340  pockthg  15534  prmgaplem5  15683  prmgaplem6  15684  drsdirfi  16859  obslbs  19993  mdetunilem9  20345  iscnp4  20977  isreg2  21091  dfconn2  21132  1stccnp  21175  flftg  21710  cnpfcf  21755  tsmsxp  21868  nmoleub  22445  vitalilem2  23284  vitalilem5  23287  c1lip1  23664  aalioulem6  23996  jensen  24615  2sqlem6  25048  dchrisumlem3  25080  pntlem3  25198  bnj849  30703  cvmlift2lem1  30992  cvmlift2lem12  31004  mclsax  31174  nn0prpwlem  31959  bj-el  32439  matunitlindflem1  33037  poimirlem30  33071  mapdordlem2  36406  iccelpart  40667  sgoldbalt  40964  evengpop3  40975  evengpoap3  40976  bgoldbtbnd  40986  lindslinindsimp1  41534