Theorem xpeq1d 5653

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-opab 5149  df-xp 5630

This theorem is referenced by:  csbres  5941  xpssres  5977  curry1  8047  fparlem3  8057  fparlem4  8058  xpord2pred  8088  xpord3pred  8095  naddcllem  8605  ixpsnf1o  8879  dfac5lem3  10038  dfac5lem4  10039  dfac5lem4OLD  10041  hashxplem  14386  repsw1  14736  subgga  19266  gasubg  19268  sylow2blem2  19587  psrval  21905  mpfrcl  22073  evlsval  22074  mamufval  22367  mat1dimscm  22450  mdetunilem3  22589  mdetunilem4  22590  mdetunilem9  22595  txindislem  23608  txtube  23615  txcmplem1  23616  txhaus  23622  xkoinjcn  23662  pt1hmeo  23781  tsmsxplem1  24128  tsmsxplem2  24129  cnmpopc  24905  dchrval  27211  axlowdimlem15  29039  axlowdim  29044  0ofval  30873  fconst7v  32708  hashxpe  32895  erlval  33334  fracbas  33381  esumcvg  34246  sxbrsigalem0  34431  sxbrsigalem3  34432  sxbrsigalem2  34446  ofcccat  34703  lpadval  34836  lpadlem3  34838  mexval2  35701  csbfinxpg  37718  poimirlem1  37956  poimirlem2  37957  poimirlem3  37958  poimirlem4  37959  poimirlem5  37960  poimirlem6  37961  poimirlem7  37962  poimirlem8  37963  poimirlem10  37965  poimirlem11  37966  poimirlem12  37967  poimirlem15  37970  poimirlem16  37971  poimirlem17  37972  poimirlem18  37973  poimirlem19  37974  poimirlem20  37975  poimirlem21  37976  poimirlem22  37977  poimirlem23  37978  poimirlem24  37979  poimirlem26  37981  poimirlem27  37982  poimirlem28  37983  poimirlem32  37987  sdclem1  38078  ismrer1  38173  ldualset  39585  dibval  41602  dibval3N  41606  dib0  41624  dihwN  41749  hdmap1fval  42256  fsuppssind  43040  mzpclval  43171  mendval  43625  dmrnxp  49324  diag1f1olem  50020  diag2f1olem  50023  prstcval  50038  prstchomval  50046