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 1542   × cxp 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-opab 5149  df-xp 5630

This theorem is referenced by:  xpriindi  5785  csbres  5941  fconstg  6721  curry2  8050  fparlem4  8058  xpord2pred  8088  xpord3pred  8095  naddcllem  8605  fvdiagfn  8832  mapsncnv  8834  xpsneng  8993  axdc4lem  10368  fpwwe2lem12  10556  indval2  12155  expval  14016  imasvscafn  17492  fuchom  17922  homafval  17987  setcmon  18045  pwsco2mhm  18792  frmdplusg  18813  smndex1igid  18865  smndex1igidOLD  18866  mulgfval  19036  mulgfvalALT  19037  mulgval  19038  efgval  19683  rngqipbas  21285  pzriprnglem13  21483  pzriprnglem14  21484  pjfval  21696  frlmval  21738  islindf5  21829  psrplusg  21926  psrvscafval  21937  psrvsca  21938  opsrle  22035  evlsvvval  22081  evlssca  22082  mpfind  22103  coe1fv  22180  coe1tm  22248  pf1ind  22330  mdetunilem4  22590  mdetunilem9  22595  txindislem  23608  txcmplem2  23617  txhaus  23622  txkgen  23627  xkofvcn  23659  xkoinjcn  23662  cnextval  24036  cnextfval  24037  pcorev2  25005  pcophtb  25006  pi1grplem  25026  pi1inv  25029  dvfval  25874  dvnfval  25899  0dgrb  26221  dgrnznn  26222  dgreq0  26240  dgrmulc  26246  plyrem  26282  facth  26283  fta1  26285  aaliou2  26317  taylfval  26335  taylpfval  26341  expsval  28431  0ofval  30873  2ndresdju  32737  aciunf1  32751  hashxpe  32895  gsumpart  33139  esplyfval2  33724  vieta  33739  ply1degltdimlem  33782  extdgfialglem1  33852  sxbrsigalem3  34432  sxbrsigalem2  34446  eulerpartlemgu  34537  sseqval  34548  sconnpht  35427  sconnpht2  35436  sconnpi1  35437  cvmlift2lem11  35511  cvmlift2lem12  35512  cvmlift2lem13  35513  cvmlift3lem9  35525  sat1el2xp  35577  mexval  35700  mexval2  35701  mdvval  35702  mpstval  35733  elima4  35974  bj-xtageq  37311  matunitlindflem1  37951  poimirlem32  37987  ismrer1  38173  ecxrncnvep2  38745  lflsc0N  39543  lkrscss  39558  lfl1dim  39581  lfl1dim2N  39582  ldualvs  39597  evlsevl  43021  0prjspnrel  43074  mzpclval  43171  mzpcl1  43175  mendvsca  43633  dvconstbi  44779  expgrowth  44780  gpgov  48530  dmrnxp  49324  fucofvalne  49812