Theorem xpeq1d 5654

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

Syntax hints:   → wi 4   = wceq 1547   × cxp 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-opab 5142  df-xp 5631

This theorem is referenced by:  csbres  5941  xpssres  5977  curry1  8050  fparlem3  8060  fparlem4  8061  xpord2pred  8092  xpord3pred  8099  naddcllem  8609  ixpsnf1o  8883  dfac5lem3  10045  dfac5lem4  10046  dfac5lem4OLD  10048  hashxplem  14393  repsw1  14743  subgga  19273  gasubg  19275  sylow2blem2  19594  psrval  21897  mpfrcl  22068  evlsval  22069  mamufval  22382  mat1dimscm  22465  mdetunilem3  22604  mdetunilem4  22605  mdetunilem9  22610  txindislem  23623  txtube  23630  txcmplem1  23631  txhaus  23637  xkoinjcn  23677  pt1hmeo  23796  tsmsxplem1  24143  tsmsxplem2  24144  cnmpopc  24920  dchrval  27222  axlowdimlem15  29050  axlowdim  29055  0ofval  30883  fconst7v  32719  hashxpe  32906  erlval  33346  fracbas  33396  esumcvg  34277  sxbrsigalem0  34462  sxbrsigalem3  34463  sxbrsigalem2  34477  ofcccat  34734  lpadval  34867  lpadlem3  34869  mexval2  35738  csbfinxpg  37757  poimirlem1  37995  poimirlem2  37996  poimirlem3  37997  poimirlem4  37998  poimirlem5  37999  poimirlem6  38000  poimirlem7  38001  poimirlem8  38002  poimirlem10  38004  poimirlem11  38005  poimirlem12  38006  poimirlem15  38009  poimirlem16  38010  poimirlem17  38011  poimirlem18  38012  poimirlem19  38013  poimirlem20  38014  poimirlem21  38015  poimirlem22  38016  poimirlem23  38017  poimirlem24  38018  poimirlem26  38020  poimirlem27  38021  poimirlem28  38022  poimirlem32  38026  sdclem1  38117  ismrer1  38212  ldualset  39624  dibval  41641  dibval3N  41645  dib0  41663  dihwN  41788  hdmap1fval  42295  fsuppssind  43050  mzpclval  43181  mendval  43631  dmrnxp  49334  diag1f1olem  50030  diag2f1olem  50033  prstcval  50048  prstchomval  50056