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  2486  dfmoeu  2536  elALT2  5316  fpropnf1  7223  findcard2d  9103  cantnflem1  9610  ttrclss  9641  ackbij1lem16  10156  fin1a2lem10  10331  inar1  10698  grur1a  10742  sqrt2irr  16186  lcmf  16572  lcmfunsnlem  16580  exprmfct  16643  pockthg  16846  prmgaplem5  16995  prmgaplem6  16996  drsdirfi  18240  obslbs  21697  mdetunilem9  22576  iscnp4  23219  isreg2  23333  dfconn2  23375  1stccnp  23418  flftg  23952  cnpfcf  23997  tsmsxp  24111  nmoleub  24687  vitalilem2  25578  vitalilem5  25581  c1lip1  25970  aalioulem6  26313  jensen  26967  2sqlem6  27402  dchrisumlem3  27470  pntlem3  27588  finsumvtxdg2sstep  29635  dfufd2lem  33641  bnj849  35100  cvmlift2lem1  35515  cvmlift2lem12  35527  mclsax  35782  nn0prpwlem  36535  mh-setindnd  36686  matunitlindflem1  37861  poimirlem30  37895  mapdordlem2  42007  eu6w  43028  iccelpart  47787  ichreuopeq  47827  sbgoldbalt  48135  sbgoldbm  48138  evengpop3  48152  evengpoap3  48153  bgoldbtbnd  48163  lindslinindsimp1  48811  iscnrm3r  49301  iscnrm3l  49304