Theorem xpeq1d 5652

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

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

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 5158  df-xp 5629

This theorem is referenced by:  csbres  5937  xpssres  5973  curry1  8044  fparlem3  8054  fparlem4  8055  xpord2pred  8085  xpord3pred  8092  naddcllem  8601  ixpsnf1o  8872  xpfiOLD  9228  dfac5lem3  10038  dfac5lem4  10039  dfac5lem4OLD  10041  hashxplem  14358  repsw1  14707  subgga  19197  gasubg  19199  sylow2blem2  19518  psrval  21840  mpfrcl  22008  evlsval  22009  mamufval  22295  mat1dimscm  22378  mdetunilem3  22517  mdetunilem4  22518  mdetunilem9  22523  txindislem  23536  txtube  23543  txcmplem1  23544  txhaus  23550  xkoinjcn  23590  pt1hmeo  23709  tsmsxplem1  24056  tsmsxplem2  24057  cnmpopc  24838  dchrval  27161  axlowdimlem15  28919  axlowdim  28924  0ofval  30749  hashxpe  32765  erlval  33211  fracbas  33257  esumcvg  34055  sxbrsigalem0  34241  sxbrsigalem3  34242  sxbrsigalem2  34256  ofcccat  34513  lpadval  34646  lpadlem3  34648  mexval2  35478  csbfinxpg  37364  poimirlem1  37603  poimirlem2  37604  poimirlem3  37605  poimirlem4  37606  poimirlem5  37607  poimirlem6  37608  poimirlem7  37609  poimirlem8  37610  poimirlem10  37612  poimirlem11  37613  poimirlem12  37614  poimirlem15  37617  poimirlem16  37618  poimirlem17  37619  poimirlem18  37620  poimirlem19  37621  poimirlem20  37622  poimirlem21  37623  poimirlem22  37624  poimirlem23  37625  poimirlem24  37626  poimirlem26  37628  poimirlem27  37629  poimirlem28  37630  poimirlem32  37634  sdclem1  37725  ismrer1  37820  ldualset  39106  dibval  41124  dibval3N  41128  dib0  41146  dihwN  41271  hdmap1fval  41778  fsuppssind  42569  mzpclval  42701  mendval  43155  dmrnxp  48825  diag1f1olem  49522  diag2f1olem  49525  prstcval  49540  prstchomval  49548