Theorem xpeq2d 5693

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

Syntax hints:   → wi 4   = wceq 1570   × cxp 5661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-opab 5175  df-xp 5669

This theorem is referenced by:  xpriindi  5824  csbres  5983  fconstg  6767  curry2  8103  fparlem4  8111  xpord2pred  8142  xpord3pred  8149  naddcllem  8663  fvdiagfn  8890  mapsncnv  8892  xpsneng  9051  axdc4lem  10440  fpwwe2lem12  10628  indval2  12224  expval  14101  imasvscafn  17592  fuchom  18022  homafval  18087  setcmon  18145  pwsco2mhm  18893  frmdplusg  18914  smndex1igid  18966  smndex1igidOLD  18967  mulgfval  19136  mulgfvalALT  19137  mulgval  19138  efgval  19788  rngqipbas  21416  pzriprnglem13  21624  pzriprnglem14  21625  pjfval  21837  frlmval  21879  islindf5  21970  psrplusg  22068  psrvscafval  22079  psrvsca  22080  opsrle  22179  evlsvvval  22225  evlssca  22226  mpfind  22247  evlsevl  22264  coe1fv  22347  coe1tm  22415  pf1ind  22496  mdetunilem4  22753  mdetunilem9  22758  txindislem  23771  txcmplem2  23780  txhaus  23785  txkgen  23790  xkofvcn  23822  xkoinjcn  23825  cnextval  24199  cnextfval  24200  pcorev2  25168  pcophtb  25169  pi1grplem  25189  pi1inv  25192  dvfval  26037  dvnfval  26062  0dgrb  26384  dgrnznn  26385  dgreq0  26403  dgrmulc  26409  plyrem  26447  facth  26448  fta1  26450  aaliou2  26484  taylfval  26503  taylpfval  26509  expsval  28599  0ofval  31120  2ndresdju  32975  aciunf1  32989  hashxpe  33133  gsumpart  33364  esplyfval2  33936  vieta  33951  ply1degltdimlem  33993  extdgfialglem1  34063  sxbrsigalem3  34643  sxbrsigalem2  34657  eulerpartlemgu  34748  sseqval  34759  sconnpht  35702  sconnpht2  35711  sconnpi1  35712  cvmlift2lem11  35786  cvmlift2lem12  35787  cvmlift2lem13  35788  cvmlift3lem9  35800  sat1el2xp  35852  mexval  35975  mexval2  35976  mdvval  35977  mpstval  36008  elima4  36249  bj-xtageq  37605  matunitlindflem1  38248  poimirlem32  38284  ismrer1  38470  ecxrncnvep2  39040  lflsc0N  39838  lkrscss  39853  lfl1dim  39876  lfl1dim2N  39877  ldualvs  39892  0prjspnrel  43342  mzpclval  43439  mzpcl1  43443  mendvsca  43897  dvconstbi  45027  expgrowth  45028  gpgov  48790  dmrnxp  49598  fucofvalne  50086