Theorem xpeq2d 5555

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

Syntax hints:   → wi 4   = wceq 1542   × cxp 5523

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-opab 5093  df-xp 5531

This theorem is referenced by:  xpriindi  5679  csbres  5828  fconstg  6565  curry2  7828  fparlem4  7836  fvdiagfn  8501  mapsncnv  8503  xpsneng  8651  axdc4lem  9955  fpwwe2lem12  10142  expval  13523  imasvscafn  16913  fuchom  17336  homafval  17401  setcmon  17459  pwsco2mhm  18113  frmdplusg  18135  smndex1igid  18185  mulgfval  18344  mulgfvalALT  18345  mulgval  18346  efgval  18961  pjfval  20522  frlmval  20564  islindf5  20655  psrplusg  20760  psrvscafval  20769  psrvsca  20770  opsrle  20858  evlssca  20903  mpfind  20921  coe1fv  20981  coe1tm  21048  pf1ind  21125  mdetunilem4  21366  mdetunilem9  21371  txindislem  22384  txcmplem2  22393  txhaus  22398  txkgen  22403  xkofvcn  22435  xkoinjcn  22438  cnextval  22812  cnextfval  22813  pcorev2  23780  pcophtb  23781  pi1grplem  23801  pi1inv  23804  dvfval  24649  dvnfval  24674  0dgrb  24995  dgrnznn  24996  dgreq0  25014  dgrmulc  25020  plyrem  25053  facth  25054  fta1  25056  aaliou2  25088  taylfval  25106  taylpfval  25112  0ofval  28722  2ndresdju  30560  aciunf1  30575  hashxpe  30702  gsumpart  30892  indval2  31552  sxbrsigalem3  31809  sxbrsigalem2  31823  eulerpartlemgu  31914  sseqval  31925  sconnpht  32762  sconnpht2  32771  sconnpi1  32772  cvmlift2lem11  32846  cvmlift2lem12  32847  cvmlift2lem13  32848  cvmlift3lem9  32860  sat1el2xp  32912  mexval  33035  mexval2  33036  mdvval  33037  mpstval  33068  elima4  33324  xpord2pred  33405  xpord3pred  33411  naddcllem  33474  bj-xtageq  34821  matunitlindflem1  35416  poimirlem32  35452  ismrer1  35639  lflsc0N  36740  lkrscss  36755  lfl1dim  36778  lfl1dim2N  36779  ldualvs  36794  evlsbagval  39874  0prjspnrel  40061  mzpclval  40139  mzpcl1  40143  mendvsca  40608  dvconstbi  41510  expgrowth  41511