MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xpeq2d Unicode version

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
StepHypRef Expression
1 xpeq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 xpeq2 4852 . 2  |-  ( A  =  B  ->  ( C  X.  A )  =  ( C  X.  B
) )
31, 2syl 16 1  |-  ( ph  ->  ( C  X.  A
)  =  ( C  X.  B ) )
Colors of variables: wff set class
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
  Copyright terms: Public domain W3C validator