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  2481  dfmoeu  2531  elALT2  5307  fpropnf1  7201  findcard2d  9076  cantnflem1  9579  ttrclss  9610  ackbij1lem16  10122  fin1a2lem10  10297  inar1  10663  grur1a  10707  sqrt2irr  16155  lcmf  16541  lcmfunsnlem  16549  exprmfct  16612  pockthg  16815  prmgaplem5  16964  prmgaplem6  16965  drsdirfi  18208  obslbs  21665  mdetunilem9  22533  iscnp4  23176  isreg2  23290  dfconn2  23332  1stccnp  23375  flftg  23909  cnpfcf  23954  tsmsxp  24068  nmoleub  24644  vitalilem2  25535  vitalilem5  25538  c1lip1  25927  aalioulem6  26270  jensen  26924  2sqlem6  27359  dchrisumlem3  27427  pntlem3  27545  finsumvtxdg2sstep  29526  dfufd2lem  33509  bnj849  34932  cvmlift2lem1  35334  cvmlift2lem12  35346  mclsax  35601  nn0prpwlem  36355  matunitlindflem1  37655  poimirlem30  37689  mapdordlem2  41675  eu6w  42708  iccelpart  47463  ichreuopeq  47503  sbgoldbalt  47811  sbgoldbm  47814  evengpop3  47828  evengpoap3  47829  bgoldbtbnd  47839  lindslinindsimp1  48488  iscnrm3r  48978  iscnrm3l  48981