Theorem xpeq2d 5705

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

Syntax hints:   → wi 4   = wceq 1541   × cxp 5673

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-opab 5210  df-xp 5681

This theorem is referenced by:  xpriindi  5834  csbres  5982  fconstg  6775  curry2  8089  fparlem4  8097  xpord2pred  8127  xpord3pred  8134  naddcllem  8671  fvdiagfn  8881  mapsncnv  8883  xpsneng  9052  axdc4lem  10446  fpwwe2lem12  10633  expval  14025  imasvscafn  17479  fuchom  17909  fuchomOLD  17910  homafval  17975  setcmon  18033  pwsco2mhm  18710  frmdplusg  18731  smndex1igid  18781  mulgfval  18946  mulgfvalALT  18947  mulgval  18948  efgval  19579  pjfval  21252  frlmval  21294  islindf5  21385  psrplusg  21491  psrvscafval  21500  psrvsca  21501  opsrle  21593  evlssca  21643  mpfind  21661  coe1fv  21721  coe1tm  21786  pf1ind  21865  mdetunilem4  22108  mdetunilem9  22113  txindislem  23128  txcmplem2  23137  txhaus  23142  txkgen  23147  xkofvcn  23179  xkoinjcn  23182  cnextval  23556  cnextfval  23557  pcorev2  24535  pcophtb  24536  pi1grplem  24556  pi1inv  24559  dvfval  25405  dvnfval  25430  0dgrb  25751  dgrnznn  25752  dgreq0  25770  dgrmulc  25776  plyrem  25809  facth  25810  fta1  25812  aaliou2  25844  taylfval  25862  taylpfval  25868  0ofval  30027  2ndresdju  31861  aciunf1  31875  hashxpe  32006  gsumpart  32194  ply1degltdimlem  32695  indval2  33000  sxbrsigalem3  33259  sxbrsigalem2  33273  eulerpartlemgu  33364  sseqval  33375  sconnpht  34208  sconnpht2  34217  sconnpi1  34218  cvmlift2lem11  34292  cvmlift2lem12  34293  cvmlift2lem13  34294  cvmlift3lem9  34306  sat1el2xp  34358  mexval  34481  mexval2  34482  mdvval  34483  mpstval  34514  elima4  34735  bj-xtageq  35857  matunitlindflem1  36472  poimirlem32  36508  ismrer1  36694  lflsc0N  37941  lkrscss  37956  lfl1dim  37979  lfl1dim2N  37980  ldualvs  37995  evlsvvval  41132  evlsevl  41140  0prjspnrel  41365  mzpclval  41448  mzpcl1  41452  mendvsca  41918  dvconstbi  43078  expgrowth  43079  rngqipbas  46760