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:  a2and  888  mo2v  2614  el  4996  fpropnf1  6688  findcard2d  8369  cantnflem1  8761  ackbij1lem16  9269  fin1a2lem10  9443  inar1  9809  grur1a  9853  sqrt2irr  15198  lcmf  15568  lcmfunsnlem  15576  exprmfct  15638  pockthg  15832  prmgaplem5  15981  prmgaplem6  15982  drsdirfi  17159  obslbs  20296  mdetunilem9  20648  iscnp4  21289  isreg2  21403  dfconn2  21444  1stccnp  21487  flftg  22021  cnpfcf  22066  tsmsxp  22179  nmoleub  22756  vitalilem2  23597  vitalilem5  23600  c1lip1  23979  aalioulem6  24311  jensen  24935  2sqlem6  25368  dchrisumlem3  25400  pntlem3  25518  finsumvtxdg2sstep  26676  bnj849  31323  cvmlift2lem1  31612  cvmlift2lem12  31624  mclsax  31794  nn0prpwlem  32644  bj-el  33124  matunitlindflem1  33736  poimirlem30  33770  mapdordlem2  37446  iccelpart  41897  sbgoldbalt  42197  sbgoldbm  42200  evengpop3  42214  evengpoap3  42215  bgoldbtbnd  42225  lindslinindsimp1  42774