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 ⊢ (𝜑 → ((𝜓 → 𝜒) → 𝜃))

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  2513  dfmoeu  2563  elALT2  5342  el  5421  fpropnf1  7267  findcard2d  9152  cantnflem1  9659  ttrclss  9690  ackbij1lem16  10218  fin1a2lem10  10394  inar1  10761  grur1a  10805  sqrt2irr  16306  lcmf  16692  lcmfunsnlem  16700  exprmfct  16764  pockthg  16967  prmgaplem5  17116  prmgaplem6  17117  drsdirfi  18362  obslbs  21861  mdetunilem9  22758  iscnp4  23401  isreg2  23515  dfconn2  23557  1stccnp  23600  flftg  24134  cnpfcf  24179  tsmsxp  24293  nmoleub  24869  vitalilem2  25749  vitalilem5  25752  c1lip1  26137  aalioulem6  26481  jensen  27134  2sqlem6  27568  dchrisumlem3  27636  pntlem3  27754  finsumvtxdg2sstep  29880  dfufd2lem  33820  bnj849  35294  cvmlift2lem1  35775  cvmlift2lem12  35787  mclsax  36042  nn0prpwlem  36814  axtco1from2  36967  mh-setindnd  37029  matunitlindflem1  38248  poimirlem30  38282  mapdordlem2  42392  eu6w  43391  iccelpart  48165  ichreuopeq  48205  sbgoldbalt  48529  sbgoldbm  48532  evengpop3  48546  evengpoap3  48547  bgoldbtbnd  48557  lindslinindsimp1  49220  iscnrm3r  49709  iscnrm3l  49712