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  2516  dfmoeu  2566  elALT2  5345  el  5424  fpropnf1  7272  findcard2d  9161  cantnflem1  9668  ttrclss  9699  ackbij1lem16  10236  fin1a2lem10  10411  inar1  10778  grur1a  10822  sqrt2irr  16330  lcmf  16716  lcmfunsnlem  16724  exprmfct  16788  pockthg  16991  prmgaplem5  17140  prmgaplem6  17141  drsdirfi  18386  obslbs  21917  mdetunilem9  22814  iscnp4  23457  isreg2  23571  dfconn2  23613  1stccnp  23656  flftg  24190  cnpfcf  24235  tsmsxp  24349  nmoleub  24925  vitalilem2  25805  vitalilem5  25808  c1lip1  26193  aalioulem6  26537  jensen  27190  2sqlem6  27624  dchrisumlem3  27692  pntlem3  27810  finsumvtxdg2sstep  29936  dfufd2lem  33870  bnj849  35345  cvmlift2lem1  35815  cvmlift2lem12  35827  mclsax  36082  nn0prpwlem  36874  axtco1from2  37027  mh-setindnd  37089  matunitlindflem1  38308  poimirlem30  38342  mapdordlem2  42452  eu6w  43449  iccelpart  48223  ichreuopeq  48263  sbgoldbalt  48587  sbgoldbm  48590  evengpop3  48604  evengpoap3  48605  bgoldbtbnd  48615  lindslinindsimp1  49278  iscnrm3r  49767  iscnrm3l  49770