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  2489  dfmoeu  2539  disj  4473  elALT2  5387  fpropnf1  7304  findcard2d  9232  cantnflem1  9758  ttrclss  9789  ackbij1lem16  10303  fin1a2lem10  10478  inar1  10844  grur1a  10888  sqrt2irr  16297  lcmf  16680  lcmfunsnlem  16688  exprmfct  16751  pockthg  16953  prmgaplem5  17102  prmgaplem6  17103  drsdirfi  18375  obslbs  21773  mdetunilem9  22647  iscnp4  23292  isreg2  23406  dfconn2  23448  1stccnp  23491  flftg  24025  cnpfcf  24070  tsmsxp  24184  nmoleub  24773  vitalilem2  25663  vitalilem5  25666  c1lip1  26056  aalioulem6  26397  jensen  27050  2sqlem6  27485  dchrisumlem3  27553  pntlem3  27671  finsumvtxdg2sstep  29585  dfufd2lem  33542  bnj849  34901  cvmlift2lem1  35270  cvmlift2lem12  35282  mclsax  35537  nn0prpwlem  36288  matunitlindflem1  37576  poimirlem30  37610  mapdordlem2  41594  eu6w  42631  iccelpart  47307  ichreuopeq  47347  sbgoldbalt  47655  sbgoldbm  47658  evengpop3  47672  evengpoap3  47673  bgoldbtbnd  47683  lindslinindsimp1  48186  iscnrm3r  48628  iscnrm3l  48631