Theorem xpeq1d 5660

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-opab 5148  df-xp 5637

This theorem is referenced by:  csbres  5947  xpssres  5983  curry1  8054  fparlem3  8064  fparlem4  8065  xpord2pred  8095  xpord3pred  8102  naddcllem  8612  ixpsnf1o  8886  dfac5lem3  10047  dfac5lem4  10048  dfac5lem4OLD  10050  hashxplem  14395  repsw1  14745  subgga  19275  gasubg  19277  sylow2blem2  19596  psrval  21895  mpfrcl  22063  evlsval  22064  mamufval  22357  mat1dimscm  22440  mdetunilem3  22579  mdetunilem4  22580  mdetunilem9  22585  txindislem  23598  txtube  23605  txcmplem1  23606  txhaus  23612  xkoinjcn  23652  pt1hmeo  23771  tsmsxplem1  24118  tsmsxplem2  24119  cnmpopc  24895  dchrval  27197  axlowdimlem15  29025  axlowdim  29030  0ofval  30858  fconst7v  32693  hashxpe  32880  erlval  33319  fracbas  33366  esumcvg  34230  sxbrsigalem0  34415  sxbrsigalem3  34416  sxbrsigalem2  34430  ofcccat  34687  lpadval  34820  lpadlem3  34822  mexval2  35685  csbfinxpg  37704  poimirlem1  37942  poimirlem2  37943  poimirlem3  37944  poimirlem4  37945  poimirlem5  37946  poimirlem6  37947  poimirlem7  37948  poimirlem8  37949  poimirlem10  37951  poimirlem11  37952  poimirlem12  37953  poimirlem15  37956  poimirlem16  37957  poimirlem17  37958  poimirlem18  37959  poimirlem19  37960  poimirlem20  37961  poimirlem21  37962  poimirlem22  37963  poimirlem23  37964  poimirlem24  37965  poimirlem26  37967  poimirlem27  37968  poimirlem28  37969  poimirlem32  37973  sdclem1  38064  ismrer1  38159  ldualset  39571  dibval  41588  dibval3N  41592  dib0  41610  dihwN  41735  hdmap1fval  42242  fsuppssind  43026  mzpclval  43157  mendval  43607  dmrnxp  49312  diag1f1olem  50008  diag2f1olem  50011  prstcval  50026  prstchomval  50034