Theorem xpeq2d 5673

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

Syntax hints:   → wi 4   = wceq 1559   × cxp 5641

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-opab 5160  df-xp 5649

This theorem is referenced by:  xpriindi  5804  csbres  5964  fconstg  6746  curry2  8080  fparlem4  8088  xpord2pred  8119  xpord3pred  8126  naddcllem  8640  fvdiagfn  8867  mapsncnv  8869  xpsneng  9028  axdc4lem  10406  fpwwe2lem12  10594  indval2  12194  expval  14070  imasvscafn  17558  fuchom  17988  homafval  18053  setcmon  18111  pwsco2mhm  18858  frmdplusg  18879  smndex1igid  18931  smndex1igidOLD  18932  mulgfval  19102  mulgfvalALT  19103  mulgval  19104  efgval  19748  rngqipbas  21353  pzriprnglem13  21533  pzriprnglem14  21534  pjfval  21746  frlmval  21788  islindf5  21879  psrplusg  21977  psrvscafval  21988  psrvsca  21989  opsrle  22088  evlsvvval  22134  evlssca  22135  mpfind  22156  evlsevl  22173  coe1fv  22256  coe1tm  22324  pf1ind  22406  mdetunilem4  22663  mdetunilem9  22668  txindislem  23681  txcmplem2  23690  txhaus  23695  txkgen  23700  xkofvcn  23732  xkoinjcn  23735  cnextval  24109  cnextfval  24110  pcorev2  25078  pcophtb  25079  pi1grplem  25099  pi1inv  25102  dvfval  25947  dvnfval  25972  0dgrb  26294  dgrnznn  26295  dgreq0  26313  dgrmulc  26319  plyrem  26357  facth  26358  fta1  26360  aaliou2  26392  taylfval  26410  taylpfval  26416  expsval  28506  0ofval  30947  2ndresdju  32812  aciunf1  32826  hashxpe  32970  gsumpart  33204  esplyfval2  33823  vieta  33838  ply1degltdimlem  33880  extdgfialglem1  33950  sxbrsigalem3  34530  sxbrsigalem2  34544  eulerpartlemgu  34635  sseqval  34646  sconnpht  35540  sconnpht2  35549  sconnpi1  35550  cvmlift2lem11  35624  cvmlift2lem12  35625  cvmlift2lem13  35626  cvmlift3lem9  35638  sat1el2xp  35690  mexval  35813  mexval2  35814  mdvval  35815  mpstval  35846  elima4  36087  bj-xtageq  37434  matunitlindflem1  38076  poimirlem32  38112  ismrer1  38298  ecxrncnvep2  38870  lflsc0N  39668  lkrscss  39683  lfl1dim  39706  lfl1dim2N  39707  ldualvs  39722  0prjspnrel  43170  mzpclval  43267  mzpcl1  43271  mendvsca  43725  dvconstbi  44871  expgrowth  44872  gpgov  48625  dmrnxp  49419  fucofvalne  49907