Theorem xpeq1d 5667

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

Syntax hints:   → wi 4   = wceq 1540   × cxp 5636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-opab 5170  df-xp 5644

This theorem is referenced by:  csbres  5953  xpssres  5989  curry1  8083  fparlem3  8093  fparlem4  8094  xpord2pred  8124  xpord3pred  8131  naddcllem  8640  ixpsnf1o  8911  xpfiOLD  9270  dfac5lem3  10078  dfac5lem4  10079  dfac5lem4OLD  10081  hashxplem  14398  repsw1  14748  subgga  19232  gasubg  19234  sylow2blem2  19551  psrval  21824  mpfrcl  21992  evlsval  21993  mamufval  22279  mat1dimscm  22362  mdetunilem3  22501  mdetunilem4  22502  mdetunilem9  22507  txindislem  23520  txtube  23527  txcmplem1  23528  txhaus  23534  xkoinjcn  23574  pt1hmeo  23693  tsmsxplem1  24040  tsmsxplem2  24041  cnmpopc  24822  dchrval  27145  axlowdimlem15  28883  axlowdim  28888  0ofval  30716  hashxpe  32732  erlval  33209  fracbas  33255  esumcvg  34076  sxbrsigalem0  34262  sxbrsigalem3  34263  sxbrsigalem2  34277  ofcccat  34534  lpadval  34667  lpadlem3  34669  mexval2  35490  csbfinxpg  37376  poimirlem1  37615  poimirlem2  37616  poimirlem3  37617  poimirlem4  37618  poimirlem5  37619  poimirlem6  37620  poimirlem7  37621  poimirlem8  37622  poimirlem10  37624  poimirlem11  37625  poimirlem12  37626  poimirlem15  37629  poimirlem16  37630  poimirlem17  37631  poimirlem18  37632  poimirlem19  37633  poimirlem20  37634  poimirlem21  37635  poimirlem22  37636  poimirlem23  37637  poimirlem24  37638  poimirlem26  37640  poimirlem27  37641  poimirlem28  37642  poimirlem32  37646  sdclem1  37737  ismrer1  37832  ldualset  39118  dibval  41136  dibval3N  41140  dib0  41158  dihwN  41283  hdmap1fval  41790  fsuppssind  42581  mzpclval  42713  mendval  43168  dmrnxp  48825  diag1f1olem  49522  diag2f1olem  49525  prstcval  49540  prstchomval  49548