Theorem xpeq1d 5672

Description: Equality deduction for Cartesian product. (Contributed by Jeff Madsen, 17-Jun-2010.)

Hypothesis

Ref	Expression
xpeq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
xpeq1d	⊢ (𝜑 → (𝐴 × 𝐶) = (𝐵 × 𝐶))

Proof of Theorem xpeq1d

Step	Hyp	Ref	Expression
1		xpeq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		xpeq1 5657	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 × 𝐶) = (𝐵 × 𝐶))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 × 𝐶) = (𝐵 × 𝐶))

Syntax hints:   → wi 4   = wceq 1559   × cxp 5641

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-opab 5160  df-xp 5649

This theorem is referenced by:  csbres  5964  xpssres  6000  curry1  8076  fparlem3  8086  fparlem4  8087  xpord2pred  8118  xpord3pred  8125  naddcllem  8639  ixpsnf1o  8913  dfac5lem3  10074  dfac5lem4  10075  dfac5lem4OLD  10077  hashxplem  14439  repsw1  14789  subgga  19330  gasubg  19332  sylow2blem2  19651  psrval  21954  mpfrcl  22125  evlsval  22126  mamufval  22439  mat1dimscm  22522  mdetunilem3  22661  mdetunilem4  22662  mdetunilem9  22667  txindislem  23680  txtube  23687  txcmplem1  23688  txhaus  23694  xkoinjcn  23734  pt1hmeo  23853  tsmsxplem1  24200  tsmsxplem2  24201  cnmpopc  24977  dchrval  27285  axlowdimlem15  29113  axlowdim  29118  0ofval  30946  fconst7v  32782  hashxpe  32969  erlval  33399  fracbas  33452  esumcvg  34343  sxbrsigalem0  34528  sxbrsigalem3  34529  sxbrsigalem2  34543  ofcccat  34800  lpadval  34933  lpadlem3  34935  mexval2  35813  csbfinxpg  37842  poimirlem1  38080  poimirlem2  38081  poimirlem3  38082  poimirlem4  38083  poimirlem5  38084  poimirlem6  38085  poimirlem7  38086  poimirlem8  38087  poimirlem10  38089  poimirlem11  38090  poimirlem12  38091  poimirlem15  38094  poimirlem16  38095  poimirlem17  38096  poimirlem18  38097  poimirlem19  38098  poimirlem20  38099  poimirlem21  38100  poimirlem22  38101  poimirlem23  38102  poimirlem24  38103  poimirlem26  38105  poimirlem27  38106  poimirlem28  38107  poimirlem32  38111  sdclem1  38202  ismrer1  38297  ldualset  39709  dibval  41726  dibval3N  41730  dib0  41748  dihwN  41873  hdmap1fval  42380  fsuppssind  43135  mzpclval  43266  mendval  43716  dmrnxp  49418  diag1f1olem  50114  diag2f1olem  50117  prstcval  50132  prstchomval  50140