Theorem xpeq2d 5681

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

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

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 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-opab 5168  df-xp 5657

This theorem is used by:  xpriindi  5813  csbres  5973  fconstg  6767  curry2  8116  fparlem4  8124  xpord2pred  8155  xpord3pred  8162  naddcllem  8678  fvdiagfn  8912  mapsncnv  8914  xpsneng  9074  axdc4lem  10526  fpwwe2lem12  10720  indval2  12318  expval  14199  imasvscafn  17702  fuchom  18132  homafval  18197  setcmon  18255  pwsco2mhm  19022  frmdplusg  19043  smndex1igid  19095  smndex1igidOLD  19096  mulgfval  19272  mulgfvalALT  19273  mulgval  19274  efgval  19924  rngqipbas  21584  pzriprnglem13  21792  pzriprnglem14  21793  pjfval  22005  frlmval  22047  islindf5  22138  psrplusg  22238  psrvscafval  22249  psrvsca  22250  opsrle  22349  evlsvvval  22395  evlssca  22396  mpfind  22417  evlsevl  22434  coe1fv  22517  coe1tm  22585  pf1ind  22666  mdetunilem4  22923  mdetunilem9  22928  matunitlindflem1  22987  txindislem  23945  txcmplem2  23954  txhaus  23959  txkgen  23964  xkofvcn  23996  xkoinjcn  23999  cnextval  24373  cnextfval  24374  pcorev2  25342  pcophtb  25343  pi1grplem  25363  pi1inv  25366  dvfval  26210  dvnfval  26235  0dgrb  26558  dgrnznn  26559  dgreq0  26577  dgrmulc  26583  plyrem  26619  facth  26620  fta1  26622  aaliou2  26660  taylfval  26679  taylpfval  26685  expsval  28804  0ofval  31382  2ndresdju  33236  aciunf1  33250  hashxpe  33392  gsumpart  33617  esplyfval2  34190  vieta  34205  ply1degltdimlem  34247  extdgfialglem1  34317  sxbrsigalem3  34897  sxbrsigalem2  34911  eulerpartlemgu  35002  sseqval  35013  sconnpht  35973  sconnpht2  35982  sconnpi1  35983  cvmlift2lem11  36057  cvmlift2lem12  36058  cvmlift2lem13  36059  cvmlift3lem9  36071  sat1el2xp  36123  mexval  36246  mexval2  36247  mdvval  36248  mpstval  36279  elima4  36520  bj-xtageq  37881  poimirlem32  38550  ismrer1  38752  ecxrncnvep2  39322  lflsc0N  40120  lkrscss  40135  lfl1dim  40158  lfl1dim2N  40159  ldualvs  40174  0prjspnrel  43643  mzpclval  43715  mzpcl1  43719  mendvsca  44173  dvconstbi  45303  expgrowth  45304  gpgov  49109  dmrnxp  49916  fucofvalne  50402