Theorem xpeq2d 5693

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   × cxp 5661

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-opab 5176  df-xp 5669

This theorem is used by:  xpriindi  5824  csbres  5983  fconstg  6769  curry2  8104  fparlem4  8112  xpord2pred  8143  xpord3pred  8150  naddcllem  8664  fvdiagfn  8891  mapsncnv  8893  xpsneng  9053  axdc4lem  10450  fpwwe2lem12  10638  indval2  12234  expval  14112  imasvscafn  17608  fuchom  18038  homafval  18103  setcmon  18161  pwsco2mhm  18915  frmdplusg  18936  smndex1igid  18988  smndex1igidOLD  18989  mulgfval  19158  mulgfvalALT  19159  mulgval  19160  efgval  19810  rngqipbas  21464  pzriprnglem13  21672  pzriprnglem14  21673  pjfval  21885  frlmval  21927  islindf5  22018  psrplusg  22116  psrvscafval  22127  psrvsca  22128  opsrle  22227  evlsvvval  22273  evlssca  22274  mpfind  22295  evlsevl  22312  coe1fv  22395  coe1tm  22463  pf1ind  22544  mdetunilem4  22801  mdetunilem9  22806  txindislem  23819  txcmplem2  23828  txhaus  23833  txkgen  23838  xkofvcn  23870  xkoinjcn  23873  cnextval  24247  cnextfval  24248  pcorev2  25216  pcophtb  25217  pi1grplem  25237  pi1inv  25240  dvfval  26085  dvnfval  26110  0dgrb  26432  dgrnznn  26433  dgreq0  26451  dgrmulc  26457  plyrem  26495  facth  26496  fta1  26498  aaliou2  26532  taylfval  26551  taylpfval  26557  expsval  28647  0ofval  31168  2ndresdju  33023  aciunf1  33037  hashxpe  33181  gsumpart  33406  esplyfval2  33978  vieta  33993  ply1degltdimlem  34035  extdgfialglem1  34105  sxbrsigalem3  34686  sxbrsigalem2  34700  eulerpartlemgu  34791  sseqval  34802  sconnpht  35734  sconnpht2  35743  sconnpi1  35744  cvmlift2lem11  35818  cvmlift2lem12  35819  cvmlift2lem13  35820  cvmlift3lem9  35832  sat1el2xp  35884  mexval  36007  mexval2  36008  mdvval  36009  mpstval  36040  elima4  36281  bj-xtageq  37657  matunitlindflem1  38300  poimirlem32  38336  ismrer1  38522  ecxrncnvep2  39092  lflsc0N  39890  lkrscss  39905  lfl1dim  39928  lfl1dim2N  39929  ldualvs  39944  0prjspnrel  43392  mzpclval  43489  mzpcl1  43493  mendvsca  43947  dvconstbi  45077  expgrowth  45078  gpgov  48840  dmrnxp  49648  fucofvalne  50136