Theorem xpeq2d 5680

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   × cxp 5648

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-opab 5167  df-xp 5656

This theorem is used by:  xpriindi  5812  csbres  5972  fconstg  6770  curry2  8121  fparlem4  8129  xpord2pred  8165  xpord3pred  8172  naddcllem  8689  fvdiagfn  8923  mapsncnv  8925  xpsneng  9085  axdc4lem  10537  fpwwe2lem12  10731  indval2  12329  expval  14210  imasvscafn  17715  fuchom  18145  homafval  18210  setcmon  18268  pwsco2mhm  19035  frmdplusg  19056  smndex1igid  19108  smndex1igidOLD  19109  mulgfval  19285  mulgfvalALT  19286  mulgval  19287  efgval  19937  rngqipbas  21597  pzriprnglem13  21805  pzriprnglem14  21806  pjfval  22018  frlmval  22060  islindf5  22151  psrplusg  22251  psrvscafval  22262  psrvsca  22263  opsrle  22362  evlsvvval  22408  evlssca  22409  mpfind  22430  evlsevl  22447  coe1fv  22530  coe1tm  22598  pf1ind  22679  mdetunilem4  22936  mdetunilem9  22941  matunitlindflem1  23000  txindislem  23958  txcmplem2  23967  txhaus  23972  txkgen  23977  xkofvcn  24009  xkoinjcn  24012  cnextval  24386  cnextfval  24387  pcorev2  25355  pcophtb  25356  pi1grplem  25376  pi1inv  25379  dvfval  26223  dvnfval  26248  0dgrb  26571  dgrnznn  26572  dgreq0  26590  dgrmulc  26596  plyrem  26632  facth  26633  fta1  26635  aaliou2  26673  taylfval  26692  taylpfval  26698  expsval  28817  0ofval  31395  2ndresdju  33291  aciunf1  33305  hashxpe  33446  gsumpart  33671  esplyfval2  34244  vieta  34259  ply1degltdimlem  34301  extdgfialglem1  34371  sxbrsigalem3  34951  sxbrsigalem2  34965  eulerpartlemgu  35056  sseqval  35067  sconnpht  36081  sconnpht2  36090  sconnpi1  36091  cvmlift2lem11  36165  cvmlift2lem12  36166  cvmlift2lem13  36167  cvmlift3lem9  36179  sat1el2xp  36231  mexval  36354  mexval2  36355  mdvval  36356  mpstval  36387  elima4  36633  bj-xtageq  37994  poimirlem32  38664  ismrer1  38866  ecxrncnvep2  39436  lflsc0N  40234  lkrscss  40249  lfl1dim  40272  lfl1dim2N  40273  ldualvs  40288  0prjspnrel  43757  mzpclval  43830  mzpcl1  43834  mendvsca  44283  dvconstbi  45412  expgrowth  45413  gpgov  49234  dmrnxp  50042  fucofvalne  50541