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  2485  dfmoeu  2535  elALT2  5311  el  5390  fpropnf1  7222  findcard2d  9101  cantnflem1  9610  ttrclss  9641  ackbij1lem16  10156  fin1a2lem10  10331  inar1  10698  grur1a  10742  sqrt2irr  16216  lcmf  16602  lcmfunsnlem  16610  exprmfct  16674  pockthg  16877  prmgaplem5  17026  prmgaplem6  17027  drsdirfi  18271  obslbs  21710  mdetunilem9  22585  iscnp4  23228  isreg2  23342  dfconn2  23384  1stccnp  23427  flftg  23961  cnpfcf  24006  tsmsxp  24120  nmoleub  24696  vitalilem2  25576  vitalilem5  25579  c1lip1  25964  aalioulem6  26303  jensen  26952  2sqlem6  27386  dchrisumlem3  27454  pntlem3  27572  finsumvtxdg2sstep  29618  dfufd2lem  33609  bnj849  35067  cvmlift2lem1  35484  cvmlift2lem12  35496  mclsax  35751  nn0prpwlem  36504  axtco1from2  36657  mh-setindnd  36719  matunitlindflem1  37937  poimirlem30  37971  mapdordlem2  42083  eu6w  43109  iccelpart  47893  ichreuopeq  47933  sbgoldbalt  48257  sbgoldbm  48260  evengpop3  48274  evengpoap3  48275  bgoldbtbnd  48285  lindslinindsimp1  48933  iscnrm3r  49423  iscnrm3l  49426