Theorem xpeq2d 5715

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-opab 5206  df-xp 5691

This theorem is referenced by:  xpriindi  5847  csbres  6000  fconstg  6795  curry2  8132  fparlem4  8140  xpord2pred  8170  xpord3pred  8177  naddcllem  8714  fvdiagfn  8931  mapsncnv  8933  xpsneng  9096  axdc4lem  10495  fpwwe2lem12  10682  expval  14104  imasvscafn  17582  fuchom  18009  homafval  18074  setcmon  18132  pwsco2mhm  18846  frmdplusg  18867  smndex1igid  18917  mulgfval  19087  mulgfvalALT  19088  mulgval  19089  efgval  19735  rngqipbas  21305  pzriprnglem13  21504  pzriprnglem14  21505  pjfval  21726  frlmval  21768  islindf5  21859  psrplusg  21956  psrvscafval  21968  psrvsca  21969  opsrle  22065  evlssca  22113  mpfind  22131  coe1fv  22208  coe1tm  22276  pf1ind  22359  mdetunilem4  22621  mdetunilem9  22626  txindislem  23641  txcmplem2  23650  txhaus  23655  txkgen  23660  xkofvcn  23692  xkoinjcn  23695  cnextval  24069  cnextfval  24070  pcorev2  25061  pcophtb  25062  pi1grplem  25082  pi1inv  25085  dvfval  25932  dvnfval  25958  0dgrb  26285  dgrnznn  26286  dgreq0  26305  dgrmulc  26311  plyrem  26347  facth  26348  fta1  26350  aaliou2  26382  taylfval  26400  taylpfval  26406  expsval  28408  0ofval  30806  2ndresdju  32659  aciunf1  32673  hashxpe  32811  indval2  32839  gsumpart  33060  ply1degltdimlem  33673  sxbrsigalem3  34274  sxbrsigalem2  34288  eulerpartlemgu  34379  sseqval  34390  sconnpht  35234  sconnpht2  35243  sconnpi1  35244  cvmlift2lem11  35318  cvmlift2lem12  35319  cvmlift2lem13  35320  cvmlift3lem9  35332  sat1el2xp  35384  mexval  35507  mexval2  35508  mdvval  35509  mpstval  35540  elima4  35776  bj-xtageq  36989  matunitlindflem1  37623  poimirlem32  37659  ismrer1  37845  lflsc0N  39084  lkrscss  39099  lfl1dim  39122  lfl1dim2N  39123  ldualvs  39138  evlsvvval  42573  evlsevl  42581  0prjspnrel  42637  mzpclval  42736  mzpcl1  42740  mendvsca  43199  dvconstbi  44353  expgrowth  44354  gpgov  48001  fucofvalne  49020