Theorem xpeq2d 5662

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

Syntax hints:   → wi 4   = wceq 1542   × cxp 5630

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-opab 5163  df-xp 5638

This theorem is referenced by:  xpriindi  5793  csbres  5949  fconstg  6729  curry2  8059  fparlem4  8067  xpord2pred  8097  xpord3pred  8104  naddcllem  8614  fvdiagfn  8841  mapsncnv  8843  xpsneng  9002  axdc4lem  10377  fpwwe2lem12  10565  expval  13998  imasvscafn  17470  fuchom  17900  homafval  17965  setcmon  18023  pwsco2mhm  18770  frmdplusg  18791  smndex1igid  18841  mulgfval  19011  mulgfvalALT  19012  mulgval  19013  efgval  19658  rngqipbas  21262  pzriprnglem13  21460  pzriprnglem14  21461  pjfval  21673  frlmval  21715  islindf5  21806  psrplusg  21904  psrvscafval  21916  psrvsca  21917  opsrle  22014  evlsvvval  22060  evlssca  22061  mpfind  22082  coe1fv  22159  coe1tm  22227  pf1ind  22311  mdetunilem4  22571  mdetunilem9  22576  txindislem  23589  txcmplem2  23598  txhaus  23603  txkgen  23608  xkofvcn  23640  xkoinjcn  23643  cnextval  24017  cnextfval  24018  pcorev2  24996  pcophtb  24997  pi1grplem  25017  pi1inv  25020  dvfval  25866  dvnfval  25892  0dgrb  26219  dgrnznn  26220  dgreq0  26239  dgrmulc  26245  plyrem  26281  facth  26282  fta1  26284  aaliou2  26316  taylfval  26334  taylpfval  26340  expsval  28433  0ofval  30874  2ndresdju  32738  aciunf1  32752  hashxpe  32897  indval2  32943  gsumpart  33156  esplyfval2  33741  vieta  33756  ply1degltdimlem  33799  extdgfialglem1  33869  sxbrsigalem3  34449  sxbrsigalem2  34463  eulerpartlemgu  34554  sseqval  34565  sconnpht  35442  sconnpht2  35451  sconnpi1  35452  cvmlift2lem11  35526  cvmlift2lem12  35527  cvmlift2lem13  35528  cvmlift3lem9  35540  sat1el2xp  35592  mexval  35715  mexval2  35716  mdvval  35717  mpstval  35748  elima4  35989  bj-xtageq  37233  matunitlindflem1  37864  poimirlem32  37900  ismrer1  38086  ecxrncnvep2  38658  lflsc0N  39456  lkrscss  39471  lfl1dim  39494  lfl1dim2N  39495  ldualvs  39510  evlsevl  42929  0prjspnrel  42982  mzpclval  43079  mzpcl1  43083  mendvsca  43541  dvconstbi  44687  expgrowth  44688  gpgov  48399  dmrnxp  49193  fucofvalne  49681