Theorem embantd 57

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 55	. 2 ⊢ (𝜑 → ((𝜓 → 𝜒) → (𝜓 → 𝜃)))
4	1, 3	mpid 43	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:  a2and  849  mo2v  2465  el  4773  findcard2d  8087  cantnflem1  8469  ackbij1lem16  8940  fin1a2lem10  9114  inar1  9476  grur1a  9520  sqrt2irr  14817  lcmf  15184  lcmfunsnlem  15192  exprmfct  15254  pockthg  15448  prmgaplem5  15597  prmgaplem6  15598  drsdirfi  16761  obslbs  19893  mdetunilem9  20245  iscnp4  20877  isreg2  20991  dfcon2  21032  1stccnp  21075  flftg  21610  cnpfcf  21655  tsmsxp  21768  nmoleub  22345  vitalilem2  23184  vitalilem5  23187  c1lip1  23564  aalioulem6  23896  jensen  24515  2sqlem6  24948  dchrisumlem3  24980  pntlem3  25098  bnj849  30249  cvmlift2lem1  30538  cvmlift2lem12  30550  mclsax  30720  nn0prpwlem  31487  bj-el  31984  matunitlindflem1  32575  poimirlem30  32609  mapdordlem2  35944  iccelpart  39971  sgoldbalt  40203  evengpop3  40214  evengpoap3  40215  bgoldbtbnd  40225  fpropnf1  40337  lindslinindsimp1  42040