Theorem xpeq2d 5707

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

Hypothesis

Ref	Expression
xpeq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
xpeq2d	⊢ (𝜑 → (𝐶 × 𝐴) = (𝐶 × 𝐵))

Proof of Theorem xpeq2d

Step	Hyp	Ref	Expression
1		xpeq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		xpeq2 5698	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 × 𝐴) = (𝐶 × 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐶 × 𝐴) = (𝐶 × 𝐵))

Syntax hints:   → wi 4   = wceq 1542   × cxp 5675

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-opab 5212  df-xp 5683

This theorem is referenced by:  xpriindi  5837  csbres  5985  fconstg  6779  curry2  8093  fparlem4  8101  xpord2pred  8131  xpord3pred  8138  naddcllem  8675  fvdiagfn  8885  mapsncnv  8887  xpsneng  9056  axdc4lem  10450  fpwwe2lem12  10637  expval  14029  imasvscafn  17483  fuchom  17913  fuchomOLD  17914  homafval  17979  setcmon  18037  pwsco2mhm  18714  frmdplusg  18735  smndex1igid  18785  mulgfval  18952  mulgfvalALT  18953  mulgval  18954  efgval  19585  pjfval  21261  frlmval  21303  islindf5  21394  psrplusg  21500  psrvscafval  21509  psrvsca  21510  opsrle  21602  evlssca  21652  mpfind  21670  coe1fv  21730  coe1tm  21795  pf1ind  21874  mdetunilem4  22117  mdetunilem9  22122  txindislem  23137  txcmplem2  23146  txhaus  23151  txkgen  23156  xkofvcn  23188  xkoinjcn  23191  cnextval  23565  cnextfval  23566  pcorev2  24544  pcophtb  24545  pi1grplem  24565  pi1inv  24568  dvfval  25414  dvnfval  25439  0dgrb  25760  dgrnznn  25761  dgreq0  25779  dgrmulc  25785  plyrem  25818  facth  25819  fta1  25821  aaliou2  25853  taylfval  25871  taylpfval  25877  0ofval  30071  2ndresdju  31905  aciunf1  31919  hashxpe  32050  gsumpart  32238  ply1degltdimlem  32738  indval2  33043  sxbrsigalem3  33302  sxbrsigalem2  33316  eulerpartlemgu  33407  sseqval  33418  sconnpht  34251  sconnpht2  34260  sconnpi1  34261  cvmlift2lem11  34335  cvmlift2lem12  34336  cvmlift2lem13  34337  cvmlift3lem9  34349  sat1el2xp  34401  mexval  34524  mexval2  34525  mdvval  34526  mpstval  34557  elima4  34778  bj-xtageq  35917  matunitlindflem1  36532  poimirlem32  36568  ismrer1  36754  lflsc0N  38001  lkrscss  38016  lfl1dim  38039  lfl1dim2N  38040  ldualvs  38055  evlsvvval  41183  evlsevl  41191  0prjspnrel  41417  mzpclval  41511  mzpcl1  41515  mendvsca  41981  dvconstbi  43141  expgrowth  43142  rngqipbas  46828  pzriprnglem13  46865  pzriprnglem14  46866