Theorem xpeq2d 5689

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

Syntax hints:   → wi 4   = wceq 1567   × cxp 5657

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-opab 5175  df-xp 5665

This theorem is referenced by:  xpriindi  5820  csbres  5979  fconstg  6763  curry2  8098  fparlem4  8106  xpord2pred  8137  xpord3pred  8144  naddcllem  8658  fvdiagfn  8885  mapsncnv  8887  xpsneng  9046  axdc4lem  10435  fpwwe2lem12  10623  indval2  12219  expval  14095  imasvscafn  17587  fuchom  18017  homafval  18082  setcmon  18140  pwsco2mhm  18888  frmdplusg  18909  smndex1igid  18961  smndex1igidOLD  18962  mulgfval  19131  mulgfvalALT  19132  mulgval  19133  efgval  19783  rngqipbas  21402  pzriprnglem13  21608  pzriprnglem14  21609  pjfval  21821  frlmval  21863  islindf5  21954  psrplusg  22052  psrvscafval  22063  psrvsca  22064  opsrle  22163  evlsvvval  22209  evlssca  22210  mpfind  22231  evlsevl  22248  coe1fv  22331  coe1tm  22399  pf1ind  22480  mdetunilem4  22737  mdetunilem9  22742  txindislem  23755  txcmplem2  23764  txhaus  23769  txkgen  23774  xkofvcn  23806  xkoinjcn  23809  cnextval  24183  cnextfval  24184  pcorev2  25152  pcophtb  25153  pi1grplem  25173  pi1inv  25176  dvfval  26021  dvnfval  26046  0dgrb  26368  dgrnznn  26369  dgreq0  26387  dgrmulc  26393  plyrem  26431  facth  26432  fta1  26434  aaliou2  26466  taylfval  26484  taylpfval  26490  expsval  28580  0ofval  31076  2ndresdju  32931  aciunf1  32945  hashxpe  33089  gsumpart  33320  esplyfval2  33896  vieta  33911  ply1degltdimlem  33953  extdgfialglem1  34023  sxbrsigalem3  34603  sxbrsigalem2  34617  eulerpartlemgu  34708  sseqval  34719  sconnpht  35616  sconnpht2  35625  sconnpi1  35626  cvmlift2lem11  35700  cvmlift2lem12  35701  cvmlift2lem13  35702  cvmlift3lem9  35714  sat1el2xp  35766  mexval  35889  mexval2  35890  mdvval  35891  mpstval  35922  elima4  36163  bj-xtageq  37508  matunitlindflem1  38150  poimirlem32  38186  ismrer1  38372  ecxrncnvep2  38944  lflsc0N  39742  lkrscss  39757  lfl1dim  39780  lfl1dim2N  39781  ldualvs  39796  0prjspnrel  43244  mzpclval  43341  mzpcl1  43345  mendvsca  43799  dvconstbi  44929  expgrowth  44930  gpgov  48689  dmrnxp  49493  fucofvalne  49981