Theorem xpeq2d 5655

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

Syntax hints:   → wi 4   = wceq 1547   × cxp 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-opab 5142  df-xp 5631

This theorem is referenced by:  xpriindi  5785  csbres  5941  fconstg  6721  curry2  8053  fparlem4  8061  xpord2pred  8092  xpord3pred  8099  naddcllem  8609  fvdiagfn  8836  mapsncnv  8838  xpsneng  8997  axdc4lem  10375  fpwwe2lem12  10563  indval2  12162  expval  14023  imasvscafn  17499  fuchom  17929  homafval  17994  setcmon  18052  pwsco2mhm  18799  frmdplusg  18820  smndex1igid  18872  smndex1igidOLD  18873  mulgfval  19043  mulgfvalALT  19044  mulgval  19045  efgval  19690  rngqipbas  21295  pzriprnglem13  21475  pzriprnglem14  21476  pjfval  21688  frlmval  21730  islindf5  21821  psrplusg  21919  psrvscafval  21930  psrvsca  21931  opsrle  22030  evlsvvval  22076  evlssca  22077  mpfind  22098  evlsevl  22115  coe1fv  22198  coe1tm  22266  pf1ind  22348  mdetunilem4  22605  mdetunilem9  22610  txindislem  23623  txcmplem2  23632  txhaus  23637  txkgen  23642  xkofvcn  23674  xkoinjcn  23677  cnextval  24051  cnextfval  24052  pcorev2  25020  pcophtb  25021  pi1grplem  25041  pi1inv  25044  dvfval  25889  dvnfval  25914  0dgrb  26236  dgrnznn  26237  dgreq0  26255  dgrmulc  26261  plyrem  26296  facth  26297  fta1  26299  aaliou2  26331  taylfval  26349  taylpfval  26355  expsval  28442  0ofval  30883  2ndresdju  32748  aciunf1  32762  hashxpe  32906  gsumpart  33151  esplyfval2  33756  vieta  33771  ply1degltdimlem  33813  extdgfialglem1  33883  sxbrsigalem3  34463  sxbrsigalem2  34477  eulerpartlemgu  34568  sseqval  34579  sconnpht  35464  sconnpht2  35473  sconnpi1  35474  cvmlift2lem11  35548  cvmlift2lem12  35549  cvmlift2lem13  35550  cvmlift3lem9  35562  sat1el2xp  35614  mexval  35737  mexval2  35738  mdvval  35739  mpstval  35770  elima4  36011  bj-xtageq  37348  matunitlindflem1  37990  poimirlem32  38026  ismrer1  38212  ecxrncnvep2  38784  lflsc0N  39582  lkrscss  39597  lfl1dim  39620  lfl1dim2N  39621  ldualvs  39636  0prjspnrel  43084  mzpclval  43181  mzpcl1  43185  mendvsca  43639  dvconstbi  44785  expgrowth  44786  gpgov  48540  dmrnxp  49334  fucofvalne  49822