Theorem xpeq2d 5646

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

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

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-opab 5154  df-xp 5622

This theorem is referenced by:  xpriindi  5776  csbres  5931  fconstg  6710  curry2  8037  fparlem4  8045  xpord2pred  8075  xpord3pred  8082  naddcllem  8591  fvdiagfn  8815  mapsncnv  8817  xpsneng  8975  axdc4lem  10346  fpwwe2lem12  10533  expval  13970  imasvscafn  17441  fuchom  17871  homafval  17936  setcmon  17994  pwsco2mhm  18741  frmdplusg  18762  smndex1igid  18812  mulgfval  18982  mulgfvalALT  18983  mulgval  18984  efgval  19630  rngqipbas  21233  pzriprnglem13  21431  pzriprnglem14  21432  pjfval  21644  frlmval  21686  islindf5  21777  psrplusg  21874  psrvscafval  21886  psrvsca  21887  opsrle  21983  evlssca  22025  mpfind  22043  coe1fv  22120  coe1tm  22188  pf1ind  22271  mdetunilem4  22531  mdetunilem9  22536  txindislem  23549  txcmplem2  23558  txhaus  23563  txkgen  23568  xkofvcn  23600  xkoinjcn  23603  cnextval  23977  cnextfval  23978  pcorev2  24956  pcophtb  24957  pi1grplem  24977  pi1inv  24980  dvfval  25826  dvnfval  25852  0dgrb  26179  dgrnznn  26180  dgreq0  26199  dgrmulc  26205  plyrem  26241  facth  26242  fta1  26244  aaliou2  26276  taylfval  26294  taylpfval  26300  expsval  28349  0ofval  30765  2ndresdju  32629  aciunf1  32643  hashxpe  32787  indval2  32833  gsumpart  33035  ply1degltdimlem  33633  extdgfialglem1  33703  sxbrsigalem3  34283  sxbrsigalem2  34297  eulerpartlemgu  34388  sseqval  34399  sconnpht  35271  sconnpht2  35280  sconnpi1  35281  cvmlift2lem11  35355  cvmlift2lem12  35356  cvmlift2lem13  35357  cvmlift3lem9  35369  sat1el2xp  35421  mexval  35544  mexval2  35545  mdvval  35546  mpstval  35577  elima4  35818  bj-xtageq  37028  matunitlindflem1  37662  poimirlem32  37698  ismrer1  37884  lflsc0N  39128  lkrscss  39143  lfl1dim  39166  lfl1dim2N  39167  ldualvs  39182  evlsvvval  42602  evlsevl  42610  0prjspnrel  42666  mzpclval  42764  mzpcl1  42768  mendvsca  43226  dvconstbi  44373  expgrowth  44374  gpgov  48079  dmrnxp  48874  fucofvalne  49363