Theorem xpeq2d 5619

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

Syntax hints:   → wi 4   = wceq 1539   × cxp 5587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-opab 5137  df-xp 5595

This theorem is referenced by:  xpriindi  5745  csbres  5894  fconstg  6661  curry2  7947  fparlem4  7955  fvdiagfn  8679  mapsncnv  8681  xpsneng  8843  axdc4lem  10211  fpwwe2lem12  10398  expval  13784  imasvscafn  17248  fuchom  17678  fuchomOLD  17679  homafval  17744  setcmon  17802  pwsco2mhm  18471  frmdplusg  18493  smndex1igid  18543  mulgfval  18702  mulgfvalALT  18703  mulgval  18704  efgval  19323  pjfval  20913  frlmval  20955  islindf5  21046  psrplusg  21150  psrvscafval  21159  psrvsca  21160  opsrle  21248  evlssca  21299  mpfind  21317  coe1fv  21377  coe1tm  21444  pf1ind  21521  mdetunilem4  21764  mdetunilem9  21769  txindislem  22784  txcmplem2  22793  txhaus  22798  txkgen  22803  xkofvcn  22835  xkoinjcn  22838  cnextval  23212  cnextfval  23213  pcorev2  24191  pcophtb  24192  pi1grplem  24212  pi1inv  24215  dvfval  25061  dvnfval  25086  0dgrb  25407  dgrnznn  25408  dgreq0  25426  dgrmulc  25432  plyrem  25465  facth  25466  fta1  25468  aaliou2  25500  taylfval  25518  taylpfval  25524  0ofval  29149  2ndresdju  30986  aciunf1  31000  hashxpe  31127  gsumpart  31315  indval2  31982  sxbrsigalem3  32239  sxbrsigalem2  32253  eulerpartlemgu  32344  sseqval  32355  sconnpht  33191  sconnpht2  33200  sconnpi1  33201  cvmlift2lem11  33275  cvmlift2lem12  33276  cvmlift2lem13  33277  cvmlift3lem9  33289  sat1el2xp  33341  mexval  33464  mexval2  33465  mdvval  33466  mpstval  33497  elima4  33750  xpord2pred  33792  xpord3pred  33798  naddcllem  33831  bj-xtageq  35178  matunitlindflem1  35773  poimirlem32  35809  ismrer1  35996  lflsc0N  37097  lkrscss  37112  lfl1dim  37135  lfl1dim2N  37136  ldualvs  37151  evlsbagval  40275  0prjspnrel  40464  mzpclval  40547  mzpcl1  40551  mendvsca  41016  dvconstbi  41952  expgrowth  41953