Theorem xpeq2d 5685

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

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

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-opab 5168  df-xp 5661

This theorem is used by:  xpriindi  5816  csbres  5975  fconstg  6762  curry2  8104  fparlem4  8112  xpord2pred  8143  xpord3pred  8150  naddcllem  8664  fvdiagfn  8898  mapsncnv  8900  xpsneng  9060  axdc4lem  10457  fpwwe2lem12  10651  indval2  12247  expval  14127  imasvscafn  17623  fuchom  18053  homafval  18118  setcmon  18176  pwsco2mhm  18942  frmdplusg  18963  smndex1igid  19015  smndex1igidOLD  19016  mulgfval  19192  mulgfvalALT  19193  mulgval  19194  efgval  19844  rngqipbas  21498  pzriprnglem13  21706  pzriprnglem14  21707  pjfval  21919  frlmval  21961  islindf5  22052  psrplusg  22152  psrvscafval  22163  psrvsca  22164  opsrle  22263  evlsvvval  22309  evlssca  22310  mpfind  22331  evlsevl  22348  coe1fv  22431  coe1tm  22499  pf1ind  22580  mdetunilem4  22837  mdetunilem9  22842  matunitlindflem1  22901  txindislem  23859  txcmplem2  23868  txhaus  23873  txkgen  23878  xkofvcn  23910  xkoinjcn  23913  cnextval  24287  cnextfval  24288  pcorev2  25256  pcophtb  25257  pi1grplem  25277  pi1inv  25280  dvfval  26124  dvnfval  26149  0dgrb  26472  dgrnznn  26473  dgreq0  26491  dgrmulc  26497  plyrem  26535  facth  26536  fta1  26538  aaliou2  26576  taylfval  26595  taylpfval  26601  expsval  28690  0ofval  31268  2ndresdju  33122  aciunf1  33136  hashxpe  33278  gsumpart  33503  esplyfval2  34075  vieta  34090  ply1degltdimlem  34132  extdgfialglem1  34202  sxbrsigalem3  34783  sxbrsigalem2  34797  eulerpartlemgu  34888  sseqval  34899  sconnpht  35808  sconnpht2  35817  sconnpi1  35818  cvmlift2lem11  35892  cvmlift2lem12  35893  cvmlift2lem13  35894  cvmlift3lem9  35906  sat1el2xp  35958  mexval  36081  mexval2  36082  mdvval  36083  mpstval  36114  elima4  36355  bj-xtageq  37732  poimirlem32  38401  ismrer1  38588  ecxrncnvep2  39158  lflsc0N  39956  lkrscss  39971  lfl1dim  39994  lfl1dim2N  39995  ldualvs  40010  0prjspnrel  43473  mzpclval  43570  mzpcl1  43574  mendvsca  44028  dvconstbi  45158  expgrowth  45159  gpgov  48958  dmrnxp  49765  fucofvalne  50251