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  2511  dfmoeu  2561  elALT2  5331  el  5406  fpropnf1  7263  findcard2d  9166  cantnflem1  9674  ttrclss  9705  ackbij1lem16  10293  fin1a2lem10  10468  inar1  10841  grur1a  10885  sqrt2irr  16397  lcmf  16788  lcmfunsnlem  16796  exprmfct  16860  pockthg  17064  prmgaplem5  17213  prmgaplem6  17214  drsdirfi  18459  obslbs  22016  mdetunilem9  22915  matunitlindflem1  22974  iscnp4  23561  isreg2  23675  dfconn2  23717  1stccnp  23761  flftg  24295  cnpfcf  24340  tsmsxp  24454  nmoleub  25030  vitalilem2  25910  vitalilem5  25913  c1lip1  26297  aalioulem6  26646  jensen  27298  2sqlem6  27732  dchrisumlem3  27800  pntlem3  27918  finsumvtxdg2sstep  30112  dfufd2lem  34063  bnj849  35538  cvmlift2lem1  36036  cvmlift2lem12  36048  mclsax  36303  nn0prpwlem  37080  axtco1from2  37233  mh-setindnd  37295  poimirlem30  38536  mapdordlem2  42662  eu6w  43641  iccelpart  48459  ichreuopeq  48499  sbgoldbalt  48823  sbgoldbm  48826  evengpop3  48840  evengpoap3  48841  bgoldbtbnd  48851  lindslinindsimp1  49513  iscnrm3r  50000  iscnrm3l  50003