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  5306  el  5385  fpropnf1  7215  findcard2d  9094  cantnflem1  9601  ttrclss  9632  ackbij1lem16  10147  fin1a2lem10  10322  inar1  10689  grur1a  10733  sqrt2irr  16207  lcmf  16593  lcmfunsnlem  16601  exprmfct  16665  pockthg  16868  prmgaplem5  17017  prmgaplem6  17018  drsdirfi  18262  obslbs  21720  mdetunilem9  22595  iscnp4  23238  isreg2  23352  dfconn2  23394  1stccnp  23437  flftg  23971  cnpfcf  24016  tsmsxp  24130  nmoleub  24706  vitalilem2  25586  vitalilem5  25589  c1lip1  25974  aalioulem6  26314  jensen  26966  2sqlem6  27400  dchrisumlem3  27468  pntlem3  27586  finsumvtxdg2sstep  29633  dfufd2lem  33624  bnj849  35083  cvmlift2lem1  35500  cvmlift2lem12  35512  mclsax  35767  nn0prpwlem  36520  axtco1from2  36673  mh-setindnd  36735  matunitlindflem1  37951  poimirlem30  37985  mapdordlem2  42097  eu6w  43123  iccelpart  47905  ichreuopeq  47945  sbgoldbalt  48269  sbgoldbm  48272  evengpop3  48286  evengpoap3  48287  bgoldbtbnd  48297  lindslinindsimp1  48945  iscnrm3r  49435  iscnrm3l  49438