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  30040  2ndresdju  31874  aciunf1  31888  hashxpe  32019  gsumpart  32207  ply1degltdimlem  32707  indval2  33012  sxbrsigalem3  33271  sxbrsigalem2  33285  eulerpartlemgu  33376  sseqval  33387  sconnpht  34220  sconnpht2  34229  sconnpi1  34230  cvmlift2lem11  34304  cvmlift2lem12  34305  cvmlift2lem13  34306  cvmlift3lem9  34318  sat1el2xp  34370  mexval  34493  mexval2  34494  mdvval  34495  mpstval  34526  elima4  34747  bj-xtageq  35869  matunitlindflem1  36484  poimirlem32  36520  ismrer1  36706  lflsc0N  37953  lkrscss  37968  lfl1dim  37991  lfl1dim2N  37992  ldualvs  38007  evlsvvval  41135  evlsevl  41143  0prjspnrel  41369  mzpclval  41463  mzpcl1  41467  mendvsca  41933  dvconstbi  43093  expgrowth  43094  rngqipbas  46780  pzriprnglem13  46817  pzriprnglem14  46818