Theorem xpeq2d 5671

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

Syntax hints:   → wi 4   = wceq 1540   × cxp 5639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-opab 5173  df-xp 5647

This theorem is referenced by:  xpriindi  5803  csbres  5956  fconstg  6750  curry2  8089  fparlem4  8097  xpord2pred  8127  xpord3pred  8134  naddcllem  8643  fvdiagfn  8867  mapsncnv  8869  xpsneng  9030  axdc4lem  10415  fpwwe2lem12  10602  expval  14035  imasvscafn  17507  fuchom  17933  homafval  17998  setcmon  18056  pwsco2mhm  18767  frmdplusg  18788  smndex1igid  18838  mulgfval  19008  mulgfvalALT  19009  mulgval  19010  efgval  19654  rngqipbas  21212  pzriprnglem13  21410  pzriprnglem14  21411  pjfval  21622  frlmval  21664  islindf5  21755  psrplusg  21852  psrvscafval  21864  psrvsca  21865  opsrle  21961  evlssca  22003  mpfind  22021  coe1fv  22098  coe1tm  22166  pf1ind  22249  mdetunilem4  22509  mdetunilem9  22514  txindislem  23527  txcmplem2  23536  txhaus  23541  txkgen  23546  xkofvcn  23578  xkoinjcn  23581  cnextval  23955  cnextfval  23956  pcorev2  24935  pcophtb  24936  pi1grplem  24956  pi1inv  24959  dvfval  25805  dvnfval  25831  0dgrb  26158  dgrnznn  26159  dgreq0  26178  dgrmulc  26184  plyrem  26220  facth  26221  fta1  26223  aaliou2  26255  taylfval  26273  taylpfval  26279  expsval  28318  0ofval  30723  2ndresdju  32580  aciunf1  32594  hashxpe  32739  indval2  32784  gsumpart  33004  ply1degltdimlem  33625  sxbrsigalem3  34270  sxbrsigalem2  34284  eulerpartlemgu  34375  sseqval  34386  sconnpht  35223  sconnpht2  35232  sconnpi1  35233  cvmlift2lem11  35307  cvmlift2lem12  35308  cvmlift2lem13  35309  cvmlift3lem9  35321  sat1el2xp  35373  mexval  35496  mexval2  35497  mdvval  35498  mpstval  35529  elima4  35770  bj-xtageq  36983  matunitlindflem1  37617  poimirlem32  37653  ismrer1  37839  lflsc0N  39083  lkrscss  39098  lfl1dim  39121  lfl1dim2N  39122  ldualvs  39137  evlsvvval  42558  evlsevl  42566  0prjspnrel  42622  mzpclval  42720  mzpcl1  42724  mendvsca  43183  dvconstbi  44330  expgrowth  44331  gpgov  48037  dmrnxp  48829  fucofvalne  49318