Theorem xpeq1d 5650

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

Syntax hints:   → wi 4   = wceq 1541   × cxp 5619

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 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-opab 5158  df-xp 5627

This theorem is referenced by:  csbres  5937  xpssres  5973  curry1  8042  fparlem3  8052  fparlem4  8053  xpord2pred  8083  xpord3pred  8090  naddcllem  8599  ixpsnf1o  8870  dfac5lem3  10025  dfac5lem4  10026  dfac5lem4OLD  10028  hashxplem  14344  repsw1  14694  subgga  19216  gasubg  19218  sylow2blem2  19537  psrval  21856  mpfrcl  22023  evlsval  22024  mamufval  22310  mat1dimscm  22393  mdetunilem3  22532  mdetunilem4  22533  mdetunilem9  22538  txindislem  23551  txtube  23558  txcmplem1  23559  txhaus  23565  xkoinjcn  23605  pt1hmeo  23724  tsmsxplem1  24071  tsmsxplem2  24072  cnmpopc  24852  dchrval  27175  axlowdimlem15  28938  axlowdim  28943  0ofval  30771  fconst7v  32607  hashxpe  32796  erlval  33234  fracbas  33280  esumcvg  34122  sxbrsigalem0  34307  sxbrsigalem3  34308  sxbrsigalem2  34322  ofcccat  34579  lpadval  34712  lpadlem3  34714  mexval2  35570  csbfinxpg  37455  poimirlem1  37684  poimirlem2  37685  poimirlem3  37686  poimirlem4  37687  poimirlem5  37688  poimirlem6  37689  poimirlem7  37690  poimirlem8  37691  poimirlem10  37693  poimirlem11  37694  poimirlem12  37695  poimirlem15  37698  poimirlem16  37699  poimirlem17  37700  poimirlem18  37701  poimirlem19  37702  poimirlem20  37703  poimirlem21  37704  poimirlem22  37705  poimirlem23  37706  poimirlem24  37707  poimirlem26  37709  poimirlem27  37710  poimirlem28  37711  poimirlem32  37715  sdclem1  37806  ismrer1  37901  ldualset  39247  dibval  41264  dibval3N  41268  dib0  41286  dihwN  41411  hdmap1fval  41918  fsuppssind  42714  mzpclval  42845  mendval  43299  dmrnxp  48964  diag1f1olem  49661  diag2f1olem  49664  prstcval  49679  prstchomval  49687