Theorem xpeq2d 5342

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

Syntax hints:   → wi 4   = wceq 1653   × cxp 5310

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2777

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-opab 4906  df-xp 5318

This theorem is referenced by:  xpriindi  5462  csbres  5603  fconstg  6307  curry2  7509  fparlem4  7517  fvdiagfn  8142  mapsncnv  8144  xpsneng  8287  xpcdaen  9293  axdc4lem  9565  fpwwe2lem13  9752  expval  13116  imasvscafn  16512  comfffval  16672  fuchom  16935  homafval  16993  setcmon  17051  xpccofval  17137  pwsco2mhm  17686  frmdplusg  17707  mulgfval  17858  mulgval  17859  symgplusg  18121  efgval  18443  psrplusg  19704  psrvscafval  19713  psrvsca  19714  opsrle  19798  evlssca  19844  mpfind  19858  coe1fv  19898  coe1tm  19965  pf1ind  20041  pjfval  20375  frlmval  20417  islindf5  20503  mdetunilem4  20747  mdetunilem9  20752  txindislem  21765  txcmplem2  21774  txhaus  21779  txkgen  21784  xkofvcn  21816  xkoinjcn  21819  cnextval  22193  cnextfval  22194  pcorev2  23155  pcophtb  23156  pi1grplem  23176  pi1inv  23179  dvfval  24002  dvnfval  24026  0dgrb  24343  dgrnznn  24344  dgreq0  24362  dgrmulc  24368  plyrem  24401  facth  24402  fta1  24404  aaliou2  24436  taylfval  24454  taylpfval  24460  0ofval  28167  aciunf1  29982  indval2  30592  sxbrsigalem3  30850  sxbrsigalem2  30864  eulerpartlemgu  30955  sseqval  30967  sconnpht  31728  sconnpht2  31737  sconnpi1  31738  cvmlift2lem11  31812  cvmlift2lem12  31813  cvmlift2lem13  31814  cvmlift3lem9  31826  mexval  31916  mexval2  31917  mdvval  31918  mpstval  31949  elima4  32191  bj-xtageq  33468  matunitlindflem1  33894  poimirlem32  33930  ismrer1  34124  lflsc0N  35104  lkrscss  35119  lfl1dim  35142  lfl1dim2N  35143  ldualvs  35158  mzpclval  38074  mzpcl1  38078  mendvsca  38546  dvconstbi  39315  expgrowth  39316