Theorem xpeq2d 5661

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

Syntax hints:   → wi 4   = wceq 1540   × cxp 5629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-opab 5165  df-xp 5637

This theorem is referenced by:  xpriindi  5790  csbres  5942  fconstg  6729  curry2  8063  fparlem4  8071  xpord2pred  8101  xpord3pred  8108  naddcllem  8617  fvdiagfn  8841  mapsncnv  8843  xpsneng  9003  axdc4lem  10384  fpwwe2lem12  10571  expval  14004  imasvscafn  17476  fuchom  17902  homafval  17967  setcmon  18025  pwsco2mhm  18736  frmdplusg  18757  smndex1igid  18807  mulgfval  18977  mulgfvalALT  18978  mulgval  18979  efgval  19623  rngqipbas  21181  pzriprnglem13  21379  pzriprnglem14  21380  pjfval  21591  frlmval  21633  islindf5  21724  psrplusg  21821  psrvscafval  21833  psrvsca  21834  opsrle  21930  evlssca  21972  mpfind  21990  coe1fv  22067  coe1tm  22135  pf1ind  22218  mdetunilem4  22478  mdetunilem9  22483  txindislem  23496  txcmplem2  23505  txhaus  23510  txkgen  23515  xkofvcn  23547  xkoinjcn  23550  cnextval  23924  cnextfval  23925  pcorev2  24904  pcophtb  24905  pi1grplem  24925  pi1inv  24928  dvfval  25774  dvnfval  25800  0dgrb  26127  dgrnznn  26128  dgreq0  26147  dgrmulc  26153  plyrem  26189  facth  26190  fta1  26192  aaliou2  26224  taylfval  26242  taylpfval  26248  expsval  28287  0ofval  30689  2ndresdju  32546  aciunf1  32560  hashxpe  32705  indval2  32750  gsumpart  32970  ply1degltdimlem  33591  sxbrsigalem3  34236  sxbrsigalem2  34250  eulerpartlemgu  34341  sseqval  34352  sconnpht  35189  sconnpht2  35198  sconnpi1  35199  cvmlift2lem11  35273  cvmlift2lem12  35274  cvmlift2lem13  35275  cvmlift3lem9  35287  sat1el2xp  35339  mexval  35462  mexval2  35463  mdvval  35464  mpstval  35495  elima4  35736  bj-xtageq  36949  matunitlindflem1  37583  poimirlem32  37619  ismrer1  37805  lflsc0N  39049  lkrscss  39064  lfl1dim  39087  lfl1dim2N  39088  ldualvs  39103  evlsvvval  42524  evlsevl  42532  0prjspnrel  42588  mzpclval  42686  mzpcl1  42690  mendvsca  43149  dvconstbi  44296  expgrowth  44297  gpgov  48006  dmrnxp  48798  fucofvalne  49287