Theorem xpeq2d 5688

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-opab 5174  df-xp 5664

This theorem is used by:  xpriindi  5823  csbres  5989  fconstg  6799  curry2  8155  fparlem4  8163  xpord2pred  8199  xpord3pred  8206  naddcllem  8723  fvdiagfn  8957  mapsncnv  8959  xpsneng  9119  axdc4lem  10572  fpwwe2lem12  10766  indval2  12365  expval  14246  imasvscafn  17759  fuchom  18189  homafval  18254  setcmon  18312  pwsco2mhm  19079  frmdplusg  19100  smndex1igid  19152  smndex1igidOLD  19153  mulgfval  19329  mulgfvalALT  19330  mulgval  19331  efgval  19982  rngqipbas  21642  pzriprnglem13  21854  pzriprnglem14  21855  pjfval  22067  frlmval  22109  islindf5  22200  psrplusg  22300  psrvscafval  22311  psrvsca  22312  opsrle  22411  evlsvvval  22457  evlssca  22458  mpfind  22479  evlsevl  22496  coe1fv  22579  coe1tm  22647  pf1ind  22728  mdetunilem4  22985  mdetunilem9  22990  matunitlindflem1  23049  txindislem  24007  txcmplem2  24016  txhaus  24021  txkgen  24026  xkofvcn  24058  xkoinjcn  24061  cnextval  24435  cnextfval  24436  pcorev2  25404  pcophtb  25405  pi1grplem  25425  pi1inv  25428  dvfval  26272  dvnfval  26297  0dgrb  26620  dgrnznn  26621  dgreq0  26639  dgrmulc  26645  plyrem  26681  facth  26682  fta1  26684  aaliou2  26724  taylfval  26743  taylpfval  26749  expsval  28868  0ofval  31446  2ndresdju  33341  aciunf1  33355  hashxpe  33495  gsumpart  33723  esplyfval2  34308  vieta  34323  ply1degltdimlem  34365  extdgfialglem1  34435  sxbrsigalem3  35015  sxbrsigalem2  35029  eulerpartlemgu  35120  sseqval  35131  sconnpht  36202  sconnpht2  36211  sconnpi1  36212  cvmlift2lem11  36286  cvmlift2lem12  36287  cvmlift2lem13  36288  cvmlift3lem9  36300  sat1el2xp  36352  mexval  36475  mexval2  36476  mdvval  36477  mpstval  36508  elima4  36755  bj-xtageq  38116  poimirlem32  38838  ismrer1  39038  ecxrncnvep2  39608  lflsc0N  40406  lkrscss  40421  lfl1dim  40444  lfl1dim2N  40445  ldualvs  40460  0prjspnrel  43929  mzpclval  44002  mzpcl1  44006  mendvsca  44450  dvconstbi  45579  expgrowth  45580  gpgov  49413  dmrnxp  50279  fucofvalne  50778