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  disj  4425  elALT2  5339  fpropnf1  7260  findcard2d  9180  cantnflem1  9703  ttrclss  9734  ackbij1lem16  10248  fin1a2lem10  10423  inar1  10789  grur1a  10833  sqrt2irr  16267  lcmf  16652  lcmfunsnlem  16660  exprmfct  16723  pockthg  16926  prmgaplem5  17075  prmgaplem6  17076  drsdirfi  18317  obslbs  21690  mdetunilem9  22558  iscnp4  23201  isreg2  23315  dfconn2  23357  1stccnp  23400  flftg  23934  cnpfcf  23979  tsmsxp  24093  nmoleub  24670  vitalilem2  25562  vitalilem5  25565  c1lip1  25954  aalioulem6  26297  jensen  26951  2sqlem6  27386  dchrisumlem3  27454  pntlem3  27572  finsumvtxdg2sstep  29529  dfufd2lem  33564  bnj849  34956  cvmlift2lem1  35324  cvmlift2lem12  35336  mclsax  35591  nn0prpwlem  36340  matunitlindflem1  37640  poimirlem30  37674  mapdordlem2  41656  eu6w  42699  iccelpart  47447  ichreuopeq  47487  sbgoldbalt  47795  sbgoldbm  47798  evengpop3  47812  evengpoap3  47813  bgoldbtbnd  47823  lindslinindsimp1  48433  iscnrm3r  48922  iscnrm3l  48925