Theorem xpeq2d 5718

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

Syntax hints:   → wi 4   = wceq 1536   × cxp 5686

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-opab 5210  df-xp 5694

This theorem is referenced by:  xpriindi  5849  csbres  6002  fconstg  6795  curry2  8130  fparlem4  8138  xpord2pred  8168  xpord3pred  8175  naddcllem  8712  fvdiagfn  8929  mapsncnv  8931  xpsneng  9094  axdc4lem  10492  fpwwe2lem12  10679  expval  14100  imasvscafn  17583  fuchom  18016  fuchomOLD  18017  homafval  18082  setcmon  18140  pwsco2mhm  18858  frmdplusg  18879  smndex1igid  18929  mulgfval  19099  mulgfvalALT  19100  mulgval  19101  efgval  19749  rngqipbas  21322  pzriprnglem13  21521  pzriprnglem14  21522  pjfval  21743  frlmval  21785  islindf5  21876  psrplusg  21973  psrvscafval  21985  psrvsca  21986  opsrle  22082  evlssca  22130  mpfind  22148  coe1fv  22223  coe1tm  22291  pf1ind  22374  mdetunilem4  22636  mdetunilem9  22641  txindislem  23656  txcmplem2  23665  txhaus  23670  txkgen  23675  xkofvcn  23707  xkoinjcn  23710  cnextval  24084  cnextfval  24085  pcorev2  25074  pcophtb  25075  pi1grplem  25095  pi1inv  25098  dvfval  25946  dvnfval  25972  0dgrb  26299  dgrnznn  26300  dgreq0  26319  dgrmulc  26325  plyrem  26361  facth  26362  fta1  26364  aaliou2  26396  taylfval  26414  taylpfval  26420  expsval  28422  0ofval  30815  2ndresdju  32665  aciunf1  32679  hashxpe  32816  gsumpart  33042  ply1degltdimlem  33649  indval2  33994  sxbrsigalem3  34253  sxbrsigalem2  34267  eulerpartlemgu  34358  sseqval  34369  sconnpht  35213  sconnpht2  35222  sconnpi1  35223  cvmlift2lem11  35297  cvmlift2lem12  35298  cvmlift2lem13  35299  cvmlift3lem9  35311  sat1el2xp  35363  mexval  35486  mexval2  35487  mdvval  35488  mpstval  35519  elima4  35756  bj-xtageq  36970  matunitlindflem1  37602  poimirlem32  37638  ismrer1  37824  lflsc0N  39064  lkrscss  39079  lfl1dim  39102  lfl1dim2N  39103  ldualvs  39118  evlsvvval  42549  evlsevl  42557  0prjspnrel  42613  mzpclval  42712  mzpcl1  42716  mendvsca  43175  dvconstbi  44329  expgrowth  44330  gpgov  47936