Theorem xpeq1d 5661

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

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

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 5163  df-xp 5638

This theorem is referenced by:  csbres  5949  xpssres  5985  curry1  8056  fparlem3  8066  fparlem4  8067  xpord2pred  8097  xpord3pred  8104  naddcllem  8614  ixpsnf1o  8888  dfac5lem3  10047  dfac5lem4  10048  dfac5lem4OLD  10050  hashxplem  14368  repsw1  14718  subgga  19241  gasubg  19243  sylow2blem2  19562  psrval  21883  mpfrcl  22052  evlsval  22053  mamufval  22348  mat1dimscm  22431  mdetunilem3  22570  mdetunilem4  22571  mdetunilem9  22576  txindislem  23589  txtube  23596  txcmplem1  23597  txhaus  23603  xkoinjcn  23643  pt1hmeo  23762  tsmsxplem1  24109  tsmsxplem2  24110  cnmpopc  24890  dchrval  27213  axlowdimlem15  29041  axlowdim  29046  0ofval  30874  fconst7v  32709  hashxpe  32897  erlval  33351  fracbas  33398  esumcvg  34263  sxbrsigalem0  34448  sxbrsigalem3  34449  sxbrsigalem2  34463  ofcccat  34720  lpadval  34853  lpadlem3  34855  mexval2  35716  csbfinxpg  37640  poimirlem1  37869  poimirlem2  37870  poimirlem3  37871  poimirlem4  37872  poimirlem5  37873  poimirlem6  37874  poimirlem7  37875  poimirlem8  37876  poimirlem10  37878  poimirlem11  37879  poimirlem12  37880  poimirlem15  37883  poimirlem16  37884  poimirlem17  37885  poimirlem18  37886  poimirlem19  37887  poimirlem20  37888  poimirlem21  37889  poimirlem22  37890  poimirlem23  37891  poimirlem24  37892  poimirlem26  37894  poimirlem27  37895  poimirlem28  37896  poimirlem32  37900  sdclem1  37991  ismrer1  38086  ldualset  39498  dibval  41515  dibval3N  41519  dib0  41537  dihwN  41662  hdmap1fval  42169  fsuppssind  42948  mzpclval  43079  mendval  43533  dmrnxp  49193  diag1f1olem  49889  diag2f1olem  49892  prstcval  49907  prstchomval  49915