Theorem xpeq2d 5653

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

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

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 5158  df-xp 5629

This theorem is referenced by:  xpriindi  5783  csbres  5937  fconstg  6715  curry2  8047  fparlem4  8055  xpord2pred  8085  xpord3pred  8092  naddcllem  8601  fvdiagfn  8825  mapsncnv  8827  xpsneng  8986  axdc4lem  10368  fpwwe2lem12  10555  expval  13988  imasvscafn  17459  fuchom  17889  homafval  17954  setcmon  18012  pwsco2mhm  18725  frmdplusg  18746  smndex1igid  18796  mulgfval  18966  mulgfvalALT  18967  mulgval  18968  efgval  19614  rngqipbas  21220  pzriprnglem13  21418  pzriprnglem14  21419  pjfval  21631  frlmval  21673  islindf5  21764  psrplusg  21861  psrvscafval  21873  psrvsca  21874  opsrle  21970  evlssca  22012  mpfind  22030  coe1fv  22107  coe1tm  22175  pf1ind  22258  mdetunilem4  22518  mdetunilem9  22523  txindislem  23536  txcmplem2  23545  txhaus  23550  txkgen  23555  xkofvcn  23587  xkoinjcn  23590  cnextval  23964  cnextfval  23965  pcorev2  24944  pcophtb  24945  pi1grplem  24965  pi1inv  24968  dvfval  25814  dvnfval  25840  0dgrb  26167  dgrnznn  26168  dgreq0  26187  dgrmulc  26193  plyrem  26229  facth  26230  fta1  26232  aaliou2  26264  taylfval  26282  taylpfval  26288  expsval  28335  0ofval  30749  2ndresdju  32606  aciunf1  32620  hashxpe  32765  indval2  32810  gsumpart  33023  ply1degltdimlem  33597  sxbrsigalem3  34242  sxbrsigalem2  34256  eulerpartlemgu  34347  sseqval  34358  sconnpht  35204  sconnpht2  35213  sconnpi1  35214  cvmlift2lem11  35288  cvmlift2lem12  35289  cvmlift2lem13  35290  cvmlift3lem9  35302  sat1el2xp  35354  mexval  35477  mexval2  35478  mdvval  35479  mpstval  35510  elima4  35751  bj-xtageq  36964  matunitlindflem1  37598  poimirlem32  37634  ismrer1  37820  lflsc0N  39064  lkrscss  39079  lfl1dim  39102  lfl1dim2N  39103  ldualvs  39118  evlsvvval  42539  evlsevl  42547  0prjspnrel  42603  mzpclval  42701  mzpcl1  42705  mendvsca  43163  dvconstbi  44310  expgrowth  44311  gpgov  48030  dmrnxp  48825  fucofvalne  49314