Theorem xpeq1d 5648

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

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

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 5155  df-xp 5625

This theorem is referenced by:  csbres  5933  xpssres  5969  curry1  8037  fparlem3  8047  fparlem4  8048  xpord2pred  8078  xpord3pred  8085  naddcllem  8594  ixpsnf1o  8865  dfac5lem3  10019  dfac5lem4  10020  dfac5lem4OLD  10022  hashxplem  14340  repsw1  14689  subgga  19179  gasubg  19181  sylow2blem2  19500  psrval  21822  mpfrcl  21990  evlsval  21991  mamufval  22277  mat1dimscm  22360  mdetunilem3  22499  mdetunilem4  22500  mdetunilem9  22505  txindislem  23518  txtube  23525  txcmplem1  23526  txhaus  23532  xkoinjcn  23572  pt1hmeo  23691  tsmsxplem1  24038  tsmsxplem2  24039  cnmpopc  24820  dchrval  27143  axlowdimlem15  28901  axlowdim  28906  0ofval  30731  fconst7v  32565  hashxpe  32753  erlval  33199  fracbas  33245  esumcvg  34059  sxbrsigalem0  34245  sxbrsigalem3  34246  sxbrsigalem2  34260  ofcccat  34517  lpadval  34650  lpadlem3  34652  mexval2  35486  csbfinxpg  37372  poimirlem1  37611  poimirlem2  37612  poimirlem3  37613  poimirlem4  37614  poimirlem5  37615  poimirlem6  37616  poimirlem7  37617  poimirlem8  37618  poimirlem10  37620  poimirlem11  37621  poimirlem12  37622  poimirlem15  37625  poimirlem16  37626  poimirlem17  37627  poimirlem18  37628  poimirlem19  37629  poimirlem20  37630  poimirlem21  37631  poimirlem22  37632  poimirlem23  37633  poimirlem24  37634  poimirlem26  37636  poimirlem27  37637  poimirlem28  37638  poimirlem32  37642  sdclem1  37733  ismrer1  37828  ldualset  39114  dibval  41131  dibval3N  41135  dib0  41153  dihwN  41278  hdmap1fval  41785  fsuppssind  42576  mzpclval  42708  mendval  43162  dmrnxp  48831  diag1f1olem  49528  diag2f1olem  49531  prstcval  49546  prstchomval  49554