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  2484  dfmoeu  2534  disj  4456  elALT2  5375  fpropnf1  7287  findcard2d  9205  cantnflem1  9727  ttrclss  9758  ackbij1lem16  10272  fin1a2lem10  10447  inar1  10813  grur1a  10857  sqrt2irr  16282  lcmf  16667  lcmfunsnlem  16675  exprmfct  16738  pockthg  16940  prmgaplem5  17089  prmgaplem6  17090  drsdirfi  18363  obslbs  21768  mdetunilem9  22642  iscnp4  23287  isreg2  23401  dfconn2  23443  1stccnp  23486  flftg  24020  cnpfcf  24065  tsmsxp  24179  nmoleub  24768  vitalilem2  25658  vitalilem5  25661  c1lip1  26051  aalioulem6  26394  jensen  27047  2sqlem6  27482  dchrisumlem3  27550  pntlem3  27668  finsumvtxdg2sstep  29582  dfufd2lem  33557  bnj849  34918  cvmlift2lem1  35287  cvmlift2lem12  35299  mclsax  35554  nn0prpwlem  36305  matunitlindflem1  37603  poimirlem30  37637  mapdordlem2  41620  eu6w  42663  iccelpart  47358  ichreuopeq  47398  sbgoldbalt  47706  sbgoldbm  47709  evengpop3  47723  evengpoap3  47724  bgoldbtbnd  47734  lindslinindsimp1  48303  iscnrm3r  48745  iscnrm3l  48748