Theorem xpeq2d 5730

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

Syntax hints:   → wi 4   = wceq 1537   × cxp 5698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-opab 5229  df-xp 5706

This theorem is referenced by:  xpriindi  5861  csbres  6012  fconstg  6808  curry2  8148  fparlem4  8156  xpord2pred  8186  xpord3pred  8193  naddcllem  8732  fvdiagfn  8949  mapsncnv  8951  xpsneng  9122  axdc4lem  10524  fpwwe2lem12  10711  expval  14114  imasvscafn  17597  fuchom  18030  fuchomOLD  18031  homafval  18096  setcmon  18154  pwsco2mhm  18868  frmdplusg  18889  smndex1igid  18939  mulgfval  19109  mulgfvalALT  19110  mulgval  19111  efgval  19759  rngqipbas  21328  pzriprnglem13  21527  pzriprnglem14  21528  pjfval  21749  frlmval  21791  islindf5  21882  psrplusg  21979  psrvscafval  21991  psrvsca  21992  opsrle  22088  evlssca  22136  mpfind  22154  coe1fv  22229  coe1tm  22297  pf1ind  22380  mdetunilem4  22642  mdetunilem9  22647  txindislem  23662  txcmplem2  23671  txhaus  23676  txkgen  23681  xkofvcn  23713  xkoinjcn  23716  cnextval  24090  cnextfval  24091  pcorev2  25080  pcophtb  25081  pi1grplem  25101  pi1inv  25104  dvfval  25952  dvnfval  25978  0dgrb  26305  dgrnznn  26306  dgreq0  26325  dgrmulc  26331  plyrem  26365  facth  26366  fta1  26368  aaliou2  26400  taylfval  26418  taylpfval  26424  expsval  28426  0ofval  30819  2ndresdju  32667  aciunf1  32681  hashxpe  32814  gsumpart  33038  ply1degltdimlem  33635  indval2  33978  sxbrsigalem3  34237  sxbrsigalem2  34251  eulerpartlemgu  34342  sseqval  34353  sconnpht  35197  sconnpht2  35206  sconnpi1  35207  cvmlift2lem11  35281  cvmlift2lem12  35282  cvmlift2lem13  35283  cvmlift3lem9  35295  sat1el2xp  35347  mexval  35470  mexval2  35471  mdvval  35472  mpstval  35503  elima4  35739  bj-xtageq  36954  matunitlindflem1  37576  poimirlem32  37612  ismrer1  37798  lflsc0N  39039  lkrscss  39054  lfl1dim  39077  lfl1dim2N  39078  ldualvs  39093  evlsvvval  42518  evlsevl  42526  0prjspnrel  42582  mzpclval  42681  mzpcl1  42685  mendvsca  43148  dvconstbi  44303  expgrowth  44304