Theorem xpeq2d 5609

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

Syntax hints:   → wi 4   = wceq 1543   × cxp 5577

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-sb 2073  df-clab 2717  df-cleq 2731  df-clel 2818  df-opab 5133  df-xp 5585

This theorem is referenced by:  xpriindi  5733  csbres  5882  fconstg  6642  curry2  7915  fparlem4  7923  fvdiagfn  8614  mapsncnv  8616  xpsneng  8774  axdc4lem  10117  fpwwe2lem12  10304  expval  13687  imasvscafn  17140  fuchom  17569  fuchomOLD  17570  homafval  17635  setcmon  17693  pwsco2mhm  18361  frmdplusg  18383  smndex1igid  18433  mulgfval  18592  mulgfvalALT  18593  mulgval  18594  efgval  19213  pjfval  20798  frlmval  20840  islindf5  20931  psrplusg  21035  psrvscafval  21044  psrvsca  21045  opsrle  21133  evlssca  21184  mpfind  21202  coe1fv  21262  coe1tm  21329  pf1ind  21406  mdetunilem4  21647  mdetunilem9  21652  txindislem  22667  txcmplem2  22676  txhaus  22681  txkgen  22686  xkofvcn  22718  xkoinjcn  22721  cnextval  23095  cnextfval  23096  pcorev2  24072  pcophtb  24073  pi1grplem  24093  pi1inv  24096  dvfval  24941  dvnfval  24966  0dgrb  25287  dgrnznn  25288  dgreq0  25306  dgrmulc  25312  plyrem  25345  facth  25346  fta1  25348  aaliou2  25380  taylfval  25398  taylpfval  25404  0ofval  29025  2ndresdju  30862  aciunf1  30877  hashxpe  31004  gsumpart  31192  indval2  31857  sxbrsigalem3  32114  sxbrsigalem2  32128  eulerpartlemgu  32219  sseqval  32230  sconnpht  33066  sconnpht2  33075  sconnpi1  33076  cvmlift2lem11  33150  cvmlift2lem12  33151  cvmlift2lem13  33152  cvmlift3lem9  33164  sat1el2xp  33216  mexval  33339  mexval2  33340  mdvval  33341  mpstval  33372  elima4  33631  xpord2pred  33694  xpord3pred  33700  naddcllem  33733  bj-xtageq  35080  matunitlindflem1  35679  poimirlem32  35715  ismrer1  35902  lflsc0N  37003  lkrscss  37018  lfl1dim  37041  lfl1dim2N  37042  ldualvs  37057  evlsbagval  40170  0prjspnrel  40357  mzpclval  40435  mzpcl1  40439  mendvsca  40904  dvconstbi  41814  expgrowth  41815