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  2480  dfmoeu  2530  disj  4416  elALT2  5327  fpropnf1  7245  findcard2d  9136  cantnflem1  9649  ttrclss  9680  ackbij1lem16  10194  fin1a2lem10  10369  inar1  10735  grur1a  10779  sqrt2irr  16224  lcmf  16610  lcmfunsnlem  16618  exprmfct  16681  pockthg  16884  prmgaplem5  17033  prmgaplem6  17034  drsdirfi  18273  obslbs  21646  mdetunilem9  22514  iscnp4  23157  isreg2  23271  dfconn2  23313  1stccnp  23356  flftg  23890  cnpfcf  23935  tsmsxp  24049  nmoleub  24626  vitalilem2  25517  vitalilem5  25520  c1lip1  25909  aalioulem6  26252  jensen  26906  2sqlem6  27341  dchrisumlem3  27409  pntlem3  27527  finsumvtxdg2sstep  29484  dfufd2lem  33527  bnj849  34922  cvmlift2lem1  35296  cvmlift2lem12  35308  mclsax  35563  nn0prpwlem  36317  matunitlindflem1  37617  poimirlem30  37651  mapdordlem2  41638  eu6w  42671  iccelpart  47438  ichreuopeq  47478  sbgoldbalt  47786  sbgoldbm  47789  evengpop3  47803  evengpoap3  47804  bgoldbtbnd  47814  lindslinindsimp1  48450  iscnrm3r  48940  iscnrm3l  48943