Theorem embantd 54

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 52	. 2
4	1, 3	mpid 41	1

Syntax hints:  ->wi 4

This theorem is referenced by:  a2and  811  mo2v  2289  mo2vOLD  2290  mo2vOLDOLD  2291  el  4634  findcard2d  7782  cantnflem1  8129  cantnflem1OLD  8152  ackbij1lem16  8636  fin1a2lem10  8810  inar1  9174  grur1a  9218  sqrt2irr  13982  exprmfct  14251  pockthg  14424  drsdirfi  15567  obslbs  18761  mdetunilem9  19122  iscnp4  19764  isreg2  19878  dfcon2  19920  1stccnp  19963  flftg  20497  cnpfcf  20542  tsmsxp  20657  nmoleub  21238  vitalilem2  22018  vitalilem5  22021  c1lip1  22398  aalioulem6  22733  jensen  23318  2sqlem6  23644  dchrisumlem3  23676  pntlem3  23794  cvmlift2lem1  28747  cvmlift2lem12  28759  mclsax  28929  nn0prpwlem  30140  lindslinindsimp1  33058  bnj849  33983  bj-el  34382  mapdordlem2  37364

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7