Theorem xpeq2d 5661

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 5652	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 × 𝐴) = (𝐶 × 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐶 × 𝐴) = (𝐶 × 𝐵))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-opab 5148  df-xp 5637

This theorem is referenced by:  xpriindi  5791  csbres  5947  fconstg  6727  curry2  8057  fparlem4  8065  xpord2pred  8095  xpord3pred  8102  naddcllem  8612  fvdiagfn  8839  mapsncnv  8841  xpsneng  9000  axdc4lem  10377  fpwwe2lem12  10565  indval2  12164  expval  14025  imasvscafn  17501  fuchom  17931  homafval  17996  setcmon  18054  pwsco2mhm  18801  frmdplusg  18822  smndex1igid  18874  smndex1igidOLD  18875  mulgfval  19045  mulgfvalALT  19046  mulgval  19047  efgval  19692  rngqipbas  21293  pzriprnglem13  21473  pzriprnglem14  21474  pjfval  21686  frlmval  21728  islindf5  21819  psrplusg  21916  psrvscafval  21927  psrvsca  21928  opsrle  22025  evlsvvval  22071  evlssca  22072  mpfind  22093  coe1fv  22170  coe1tm  22238  pf1ind  22320  mdetunilem4  22580  mdetunilem9  22585  txindislem  23598  txcmplem2  23607  txhaus  23612  txkgen  23617  xkofvcn  23649  xkoinjcn  23652  cnextval  24026  cnextfval  24027  pcorev2  24995  pcophtb  24996  pi1grplem  25016  pi1inv  25019  dvfval  25864  dvnfval  25889  0dgrb  26211  dgrnznn  26212  dgreq0  26230  dgrmulc  26236  plyrem  26271  facth  26272  fta1  26274  aaliou2  26306  taylfval  26324  taylpfval  26330  expsval  28417  0ofval  30858  2ndresdju  32722  aciunf1  32736  hashxpe  32880  gsumpart  33124  esplyfval2  33709  vieta  33724  ply1degltdimlem  33766  extdgfialglem1  33836  sxbrsigalem3  34416  sxbrsigalem2  34430  eulerpartlemgu  34521  sseqval  34532  sconnpht  35411  sconnpht2  35420  sconnpi1  35421  cvmlift2lem11  35495  cvmlift2lem12  35496  cvmlift2lem13  35497  cvmlift3lem9  35509  sat1el2xp  35561  mexval  35684  mexval2  35685  mdvval  35686  mpstval  35717  elima4  35958  bj-xtageq  37295  matunitlindflem1  37937  poimirlem32  37973  ismrer1  38159  ecxrncnvep2  38731  lflsc0N  39529  lkrscss  39544  lfl1dim  39567  lfl1dim2N  39568  ldualvs  39583  evlsevl  43007  0prjspnrel  43060  mzpclval  43157  mzpcl1  43161  mendvsca  43615  dvconstbi  44761  expgrowth  44762  gpgov  48518  dmrnxp  49312  fucofvalne  49800