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

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  dfsb1  2510  dfmoeu  2560  elALT2  5330  el  5405  fpropnf1  7271  findcard2d  9185  cantnflem1  9693  ttrclss  9724  ackbij1lem16  10315  fin1a2lem10  10490  inar1  10863  grur1a  10907  sqrt2irr  16422  lcmf  16813  lcmfunsnlem  16821  exprmfct  16885  pockthg  17089  prmgaplem5  17238  prmgaplem6  17239  drsdirfi  18484  obslbs  22041  mdetunilem9  22940  matunitlindflem1  22999  iscnp4  23586  isreg2  23700  dfconn2  23742  1stccnp  23786  flftg  24320  cnpfcf  24365  tsmsxp  24479  nmoleub  25055  vitalilem2  25935  vitalilem5  25938  c1lip1  26322  aalioulem6  26669  jensen  27321  2sqlem6  27755  dchrisumlem3  27823  pntlem3  27941  finsumvtxdg2sstep  30135  dfufd2lem  34127  bnj849  35601  cvmlift2lem1  36153  cvmlift2lem12  36165  mclsax  36420  nn0prpwlem  37202  axtco1from2  37355  mh-setindnd  37417  poimirlem30  38661  mapdordlem2  42787  eu6w  43780  iccelpart  48608  ichreuopeq  48648  sbgoldbalt  48972  sbgoldbm  48975  evengpop3  48989  evengpoap3  48990  bgoldbtbnd  49000  lindslinindsimp1  49662  iscnrm3r  50155  iscnrm3l  50158