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  2511  dfmoeu  2561  elALT2  5325  el  5404  fpropnf1  7247  findcard2d  9131  cantnflem1  9641  ttrclss  9672  ackbij1lem16  10187  fin1a2lem10  10363  inar1  10730  grur1a  10774  sqrt2irr  16264  lcmf  16650  lcmfunsnlem  16658  exprmfct  16722  pockthg  16925  prmgaplem5  17074  prmgaplem6  17075  drsdirfi  18320  obslbs  21762  mdetunilem9  22660  iscnp4  23303  isreg2  23417  dfconn2  23459  1stccnp  23502  flftg  24036  cnpfcf  24081  tsmsxp  24195  nmoleub  24771  vitalilem2  25651  vitalilem5  25654  c1lip1  26039  aalioulem6  26378  jensen  27030  2sqlem6  27464  dchrisumlem3  27532  pntlem3  27650  finsumvtxdg2sstep  29696  dfufd2lem  33706  bnj849  35184  cvmlift2lem1  35616  cvmlift2lem12  35628  mclsax  35883  nn0prpwlem  36646  axtco1from2  36799  mh-setindnd  36861  matunitlindflem1  38079  poimirlem30  38113  mapdordlem2  42225  eu6w  43222  iccelpart  48003  ichreuopeq  48043  sbgoldbalt  48367  sbgoldbm  48370  evengpop3  48384  evengpoap3  48385  bgoldbtbnd  48395  lindslinindsimp1  49043  iscnrm3r  49533  iscnrm3l  49536