Theorem xpeq1d 5609

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

Syntax hints:   → wi 4   = wceq 1539   × cxp 5578

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-opab 5133  df-xp 5586

This theorem is referenced by:  csbres  5883  xpssres  5917  curry1  7915  fparlem3  7925  fparlem4  7926  ixpsnf1o  8684  xpfi  9015  dfac5lem3  9812  dfac5lem4  9813  hashxplem  14076  repsw1  14424  subgga  18821  gasubg  18823  sylow2blem2  19141  psrval  21028  mpfrcl  21205  evlsval  21206  mamufval  21444  mat1dimscm  21532  mdetunilem3  21671  mdetunilem4  21672  mdetunilem9  21677  txindislem  22692  txtube  22699  txcmplem1  22700  txhaus  22706  xkoinjcn  22746  pt1hmeo  22865  tsmsxplem1  23212  tsmsxplem2  23213  cnmpopc  23997  dchrval  26287  axlowdimlem15  27227  axlowdim  27232  0ofval  29050  hashxpe  31029  esumcvg  31954  sxbrsigalem0  32138  sxbrsigalem3  32139  sxbrsigalem2  32153  ofcccat  32422  lpadval  32556  lpadlem3  32558  mexval2  33365  xpord2pred  33719  xpord3pred  33725  naddcllem  33758  csbfinxpg  35486  poimirlem1  35705  poimirlem2  35706  poimirlem3  35707  poimirlem4  35708  poimirlem5  35709  poimirlem6  35710  poimirlem7  35711  poimirlem8  35712  poimirlem10  35714  poimirlem11  35715  poimirlem12  35716  poimirlem15  35719  poimirlem16  35720  poimirlem17  35721  poimirlem18  35722  poimirlem19  35723  poimirlem20  35724  poimirlem21  35725  poimirlem22  35726  poimirlem23  35727  poimirlem24  35728  poimirlem26  35730  poimirlem27  35731  poimirlem28  35732  poimirlem32  35736  sdclem1  35828  ismrer1  35923  ldualset  37066  dibval  39083  dibval3N  39087  dib0  39105  dihwN  39230  hdmap1fval  39737  fsuppssind  40205  mzpclval  40463  mendval  40924  prstcval  46233  prstchomval  46241