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  2485  dfmoeu  2535  disj  4425  elALT2  5339  fpropnf1  7259  findcard2d  9178  cantnflem1  9701  ttrclss  9732  ackbij1lem16  10246  fin1a2lem10  10421  inar1  10787  grur1a  10831  sqrt2irr  16265  lcmf  16650  lcmfunsnlem  16658  exprmfct  16721  pockthg  16924  prmgaplem5  17073  prmgaplem6  17074  drsdirfi  18315  obslbs  21688  mdetunilem9  22556  iscnp4  23199  isreg2  23313  dfconn2  23355  1stccnp  23398  flftg  23932  cnpfcf  23977  tsmsxp  24091  nmoleub  24668  vitalilem2  25560  vitalilem5  25563  c1lip1  25952  aalioulem6  26295  jensen  26949  2sqlem6  27384  dchrisumlem3  27452  pntlem3  27570  finsumvtxdg2sstep  29475  dfufd2lem  33510  bnj849  34902  cvmlift2lem1  35270  cvmlift2lem12  35282  mclsax  35537  nn0prpwlem  36286  matunitlindflem1  37586  poimirlem30  37620  mapdordlem2  41602  eu6w  42646  iccelpart  47395  ichreuopeq  47435  sbgoldbalt  47743  sbgoldbm  47746  evengpop3  47760  evengpoap3  47761  bgoldbtbnd  47771  lindslinindsimp1  48381  iscnrm3r  48870  iscnrm3l  48873