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  2481  dfmoeu  2531  disj  4448  elALT2  5368  fpropnf1  7266  findcard2d  9166  cantnflem1  9684  ttrclss  9715  ackbij1lem16  10230  fin1a2lem10  10404  inar1  10770  grur1a  10814  sqrt2irr  16192  lcmf  16570  lcmfunsnlem  16578  exprmfct  16641  pockthg  16839  prmgaplem5  16988  prmgaplem6  16989  drsdirfi  18258  obslbs  21285  mdetunilem9  22122  iscnp4  22767  isreg2  22881  dfconn2  22923  1stccnp  22966  flftg  23500  cnpfcf  23545  tsmsxp  23659  nmoleub  24248  vitalilem2  25126  vitalilem5  25129  c1lip1  25514  aalioulem6  25850  jensen  26493  2sqlem6  26926  dchrisumlem3  26994  pntlem3  27112  finsumvtxdg2sstep  28806  bnj849  33936  cvmlift2lem1  34293  cvmlift2lem12  34305  mclsax  34560  nn0prpwlem  35207  matunitlindflem1  36484  poimirlem30  36518  mapdordlem2  40508  iccelpart  46101  ichreuopeq  46141  sbgoldbalt  46449  sbgoldbm  46452  evengpop3  46466  evengpoap3  46467  bgoldbtbnd  46477  lindslinindsimp1  47138  iscnrm3r  47581  iscnrm3l  47584