Theorem xpeq2d 4861

Description: Equality deduction for cross product. (Contributed by Jeff Madsen, 17-Jun-2010.)

Hypothesis

Ref	Expression
xpeq1d.1	|- ( ph -> A = B )

Assertion

Ref	Expression
xpeq2d	|- ( ph -> ( C X. A ) = ( C X. B ) )

Proof of Theorem xpeq2d

Step	Hyp	Ref	Expression
1		xpeq1d.1	. 2 |- ( ph -> A = B )
2		xpeq2 4852	. 2 |- ( A = B -> ( C X. A ) = ( C X. B ) )
3	1, 2	syl 16	1 |- ( ph -> ( C X. A ) = ( C X. B ) )

Syntax hints:   -> wi 4   = wceq 1649   X. cxp 4835

This theorem is referenced by:  xpriindi  4970  csbresg  5108  fconstg  5589  curry2  6400  fparlem4  6408  fvdiagfn  7017  mapsncnv  7019  xpsneng  7152  xpcdaen  8019  axdc4lem  8291  fpwwe2lem13  8473  expval  11339  imasvscafn  13717  comfffval  13879  fuchom  14113  homafval  14139  setcmon  14197  xpccofval  14234  pwsco2mhm  14725  frmdplusg  14754  mulgfval  14846  mulgval  14847  symgplusg  15054  efgval  15304  psrplusg  16400  psrvscafval  16409  psrvsca  16410  opsrle  16491  coe1fv  16559  coe1tm  16620  pjfval  16888  txindislem  17618  txcmplem2  17627  txhaus  17632  txkgen  17637  xkofvcn  17669  xkoinjcn  17672  cnextval  18045  cnextfval  18046  pcorev2  19006  pcophtb  19007  pi1grplem  19027  pi1inv  19030  dvfval  19737  dvnfval  19761  evlssca  19896  mpfind  19918  pf1ind  19928  0dgrb  20118  dgreq0  20136  dgrmulc  20142  plyrem  20175  facth  20176  fta1  20178  aaliou2  20210  taylfval  20228  taylpfval  20234  gxval  21799  0ofval  22241  indval2  24365  sxbrsigalem3  24575  sxbrsigalem2  24589  sconpht  24869  sconpht2  24878  sconpi1  24879  cvmlift2lem11  24953  cvmlift2lem12  24954  cvmlift2lem13  24955  cvmlift3lem9  24967  ismrer1  26437  mzpclval  26672  mzpcl1  26676  frlmval  27084  islindf5  27177  dgrnznn  27208  mendvsca  27367  dvconstbi  27419  expgrowth  27420  lflsc0N  29566  lkrscss  29581  lfl1dim  29604  lfl1dim2N  29605  ldualvs  29620

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-opab 4227  df-xp 4843