Theorem xpeq2d 5063

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

Syntax hints:   → wi 4   = wceq 1475   × cxp 5036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-opab 4644  df-xp 5044

This theorem is referenced by:  xpriindi  5180  csbres  5320  fconstg  6005  curry2  7159  fparlem4  7167  fvdiagfn  7788  mapsncnv  7790  xpsneng  7930  xpcdaen  8888  axdc4lem  9160  fpwwe2lem13  9343  expval  12724  imasvscafn  16020  comfffval  16181  fuchom  16444  homafval  16502  setcmon  16560  xpccofval  16645  pwsco2mhm  17194  frmdplusg  17214  mulgfval  17365  mulgval  17366  symgplusg  17632  efgval  17953  psrplusg  19202  psrvscafval  19211  psrvsca  19212  opsrle  19296  evlssca  19343  mpfind  19357  coe1fv  19397  coe1tm  19464  pf1ind  19540  pjfval  19869  frlmval  19911  islindf5  19997  mdetunilem4  20240  mdetunilem9  20245  txindislem  21246  txcmplem2  21255  txhaus  21260  txkgen  21265  xkofvcn  21297  xkoinjcn  21300  cnextval  21675  cnextfval  21676  pcorev2  22636  pcophtb  22637  pi1grplem  22657  pi1inv  22660  dvfval  23467  dvnfval  23491  0dgrb  23806  dgrnznn  23807  dgreq0  23825  dgrmulc  23831  plyrem  23864  facth  23865  fta1  23867  aaliou2  23899  taylfval  23917  taylpfval  23923  0ofval  27026  aciunf1  28845  indval2  29404  sxbrsigalem3  29661  sxbrsigalem2  29675  eulerpartlemgu  29766  sseqval  29777  sconpht  30465  sconpht2  30474  sconpi1  30475  cvmlift2lem11  30549  cvmlift2lem12  30550  cvmlift2lem13  30551  cvmlift3lem9  30563  mexval  30653  mexval2  30654  mdvval  30655  mpstval  30686  elima4  30924  bj-xtageq  32169  matunitlindflem1  32575  poimirlem32  32611  ismrer1  32807  lflsc0N  33388  lkrscss  33403  lfl1dim  33426  lfl1dim2N  33427  ldualvs  33442  mzpclval  36306  mzpcl1  36310  mendvsca  36780  dvconstbi  37555  expgrowth  37556  csbresgOLD  38077