Theorem xpeq2d 5668

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

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-opab 5170  df-xp 5644

This theorem is referenced by:  xpriindi  5800  csbres  5953  fconstg  6747  curry2  8086  fparlem4  8094  xpord2pred  8124  xpord3pred  8131  naddcllem  8640  fvdiagfn  8864  mapsncnv  8866  xpsneng  9026  axdc4lem  10408  fpwwe2lem12  10595  expval  14028  imasvscafn  17500  fuchom  17926  homafval  17991  setcmon  18049  pwsco2mhm  18760  frmdplusg  18781  smndex1igid  18831  mulgfval  19001  mulgfvalALT  19002  mulgval  19003  efgval  19647  rngqipbas  21205  pzriprnglem13  21403  pzriprnglem14  21404  pjfval  21615  frlmval  21657  islindf5  21748  psrplusg  21845  psrvscafval  21857  psrvsca  21858  opsrle  21954  evlssca  21996  mpfind  22014  coe1fv  22091  coe1tm  22159  pf1ind  22242  mdetunilem4  22502  mdetunilem9  22507  txindislem  23520  txcmplem2  23529  txhaus  23534  txkgen  23539  xkofvcn  23571  xkoinjcn  23574  cnextval  23948  cnextfval  23949  pcorev2  24928  pcophtb  24929  pi1grplem  24949  pi1inv  24952  dvfval  25798  dvnfval  25824  0dgrb  26151  dgrnznn  26152  dgreq0  26171  dgrmulc  26177  plyrem  26213  facth  26214  fta1  26216  aaliou2  26248  taylfval  26266  taylpfval  26272  expsval  28311  0ofval  30716  2ndresdju  32573  aciunf1  32587  hashxpe  32732  indval2  32777  gsumpart  32997  ply1degltdimlem  33618  sxbrsigalem3  34263  sxbrsigalem2  34277  eulerpartlemgu  34368  sseqval  34379  sconnpht  35216  sconnpht2  35225  sconnpi1  35226  cvmlift2lem11  35300  cvmlift2lem12  35301  cvmlift2lem13  35302  cvmlift3lem9  35314  sat1el2xp  35366  mexval  35489  mexval2  35490  mdvval  35491  mpstval  35522  elima4  35763  bj-xtageq  36976  matunitlindflem1  37610  poimirlem32  37646  ismrer1  37832  lflsc0N  39076  lkrscss  39091  lfl1dim  39114  lfl1dim2N  39115  ldualvs  39130  evlsvvval  42551  evlsevl  42559  0prjspnrel  42615  mzpclval  42713  mzpcl1  42717  mendvsca  43176  dvconstbi  44323  expgrowth  44324  gpgov  48033  dmrnxp  48825  fucofvalne  49314