Theorem xpeq2d 5654

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

Syntax hints:   → wi 4   = wceq 1541   × cxp 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-opab 5161  df-xp 5630

This theorem is referenced by:  xpriindi  5785  csbres  5941  fconstg  6721  curry2  8049  fparlem4  8057  xpord2pred  8087  xpord3pred  8094  naddcllem  8604  fvdiagfn  8829  mapsncnv  8831  xpsneng  8990  axdc4lem  10365  fpwwe2lem12  10553  expval  13986  imasvscafn  17458  fuchom  17888  homafval  17953  setcmon  18011  pwsco2mhm  18758  frmdplusg  18779  smndex1igid  18829  mulgfval  18999  mulgfvalALT  19000  mulgval  19001  efgval  19646  rngqipbas  21250  pzriprnglem13  21448  pzriprnglem14  21449  pjfval  21661  frlmval  21703  islindf5  21794  psrplusg  21892  psrvscafval  21904  psrvsca  21905  opsrle  22002  evlsvvval  22048  evlssca  22049  mpfind  22070  coe1fv  22147  coe1tm  22215  pf1ind  22299  mdetunilem4  22559  mdetunilem9  22564  txindislem  23577  txcmplem2  23586  txhaus  23591  txkgen  23596  xkofvcn  23628  xkoinjcn  23631  cnextval  24005  cnextfval  24006  pcorev2  24984  pcophtb  24985  pi1grplem  25005  pi1inv  25008  dvfval  25854  dvnfval  25880  0dgrb  26207  dgrnznn  26208  dgreq0  26227  dgrmulc  26233  plyrem  26269  facth  26270  fta1  26272  aaliou2  26304  taylfval  26322  taylpfval  26328  expsval  28421  0ofval  30862  2ndresdju  32727  aciunf1  32741  hashxpe  32887  indval2  32933  gsumpart  33146  esplyfval2  33723  vieta  33736  ply1degltdimlem  33779  extdgfialglem1  33849  sxbrsigalem3  34429  sxbrsigalem2  34443  eulerpartlemgu  34534  sseqval  34545  sconnpht  35423  sconnpht2  35432  sconnpi1  35433  cvmlift2lem11  35507  cvmlift2lem12  35508  cvmlift2lem13  35509  cvmlift3lem9  35521  sat1el2xp  35573  mexval  35696  mexval2  35697  mdvval  35698  mpstval  35729  elima4  35970  bj-xtageq  37189  matunitlindflem1  37817  poimirlem32  37853  ismrer1  38039  ecxrncnvep2  38595  lflsc0N  39343  lkrscss  39358  lfl1dim  39381  lfl1dim2N  39382  ldualvs  39397  evlsevl  42817  0prjspnrel  42870  mzpclval  42967  mzpcl1  42971  mendvsca  43429  dvconstbi  44575  expgrowth  44576  gpgov  48288  dmrnxp  49082  fucofvalne  49570