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 1541   × cxp 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-opab 5161  df-xp 5630

This theorem is referenced by:  csbres  5941  xpssres  5977  curry1  8046  fparlem3  8056  fparlem4  8057  xpord2pred  8087  xpord3pred  8094  naddcllem  8604  ixpsnf1o  8876  dfac5lem3  10035  dfac5lem4  10036  dfac5lem4OLD  10038  hashxplem  14356  repsw1  14706  subgga  19229  gasubg  19231  sylow2blem2  19550  psrval  21871  mpfrcl  22040  evlsval  22041  mamufval  22336  mat1dimscm  22419  mdetunilem3  22558  mdetunilem4  22559  mdetunilem9  22564  txindislem  23577  txtube  23584  txcmplem1  23585  txhaus  23591  xkoinjcn  23631  pt1hmeo  23750  tsmsxplem1  24097  tsmsxplem2  24098  cnmpopc  24878  dchrval  27201  axlowdimlem15  29029  axlowdim  29034  0ofval  30862  fconst7v  32698  hashxpe  32887  erlval  33340  fracbas  33387  esumcvg  34243  sxbrsigalem0  34428  sxbrsigalem3  34429  sxbrsigalem2  34443  ofcccat  34700  lpadval  34833  lpadlem3  34835  mexval2  35697  csbfinxpg  37593  poimirlem1  37822  poimirlem2  37823  poimirlem3  37824  poimirlem4  37825  poimirlem5  37826  poimirlem6  37827  poimirlem7  37828  poimirlem8  37829  poimirlem10  37831  poimirlem11  37832  poimirlem12  37833  poimirlem15  37836  poimirlem16  37837  poimirlem17  37838  poimirlem18  37839  poimirlem19  37840  poimirlem20  37841  poimirlem21  37842  poimirlem22  37843  poimirlem23  37844  poimirlem24  37845  poimirlem26  37847  poimirlem27  37848  poimirlem28  37849  poimirlem32  37853  sdclem1  37944  ismrer1  38039  ldualset  39385  dibval  41402  dibval3N  41406  dib0  41424  dihwN  41549  hdmap1fval  42056  fsuppssind  42836  mzpclval  42967  mendval  43421  dmrnxp  49082  diag1f1olem  49778  diag2f1olem  49781  prstcval  49796  prstchomval  49804