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 ⊢ (𝜑 → ((𝜓 → 𝜒) → 𝜃))

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  2515  dfmoeu  2565  elALT2  5331  el  5410  fpropnf1  7255  findcard2d  9139  cantnflem1  9646  ttrclss  9677  ackbij1lem16  10205  fin1a2lem10  10381  inar1  10748  grur1a  10792  sqrt2irr  16295  lcmf  16681  lcmfunsnlem  16689  exprmfct  16753  pockthg  16956  prmgaplem5  17105  prmgaplem6  17106  drsdirfi  18351  obslbs  21840  mdetunilem9  22738  iscnp4  23381  isreg2  23495  dfconn2  23537  1stccnp  23580  flftg  24114  cnpfcf  24159  tsmsxp  24273  nmoleub  24849  vitalilem2  25729  vitalilem5  25732  c1lip1  26117  aalioulem6  26459  jensen  27111  2sqlem6  27545  dchrisumlem3  27613  pntlem3  27731  finsumvtxdg2sstep  29808  dfufd2lem  33756  bnj849  35230  cvmlift2lem1  35665  cvmlift2lem12  35677  mclsax  35932  nn0prpwlem  36695  axtco1from2  36848  mh-setindnd  36910  matunitlindflem1  38127  poimirlem30  38161  mapdordlem2  42273  eu6w  43270  iccelpart  48037  ichreuopeq  48077  sbgoldbalt  48401  sbgoldbm  48404  evengpop3  48418  evengpoap3  48419  bgoldbtbnd  48429  lindslinindsimp1  49088  iscnrm3r  49577  iscnrm3l  49580