Theorem xpeq1d 5619

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

Syntax hints:   → wi 4   = wceq 1539   × cxp 5588

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-opab 5138  df-xp 5596

This theorem is referenced by:  csbres  5897  xpssres  5931  curry1  7953  fparlem3  7963  fparlem4  7964  ixpsnf1o  8735  xpfi  9094  dfac5lem3  9890  dfac5lem4  9891  hashxplem  14157  repsw1  14505  subgga  18915  gasubg  18917  sylow2blem2  19235  psrval  21127  mpfrcl  21304  evlsval  21305  mamufval  21543  mat1dimscm  21633  mdetunilem3  21772  mdetunilem4  21773  mdetunilem9  21778  txindislem  22793  txtube  22800  txcmplem1  22801  txhaus  22807  xkoinjcn  22847  pt1hmeo  22966  tsmsxplem1  23313  tsmsxplem2  23314  cnmpopc  24100  dchrval  26391  axlowdimlem15  27333  axlowdim  27338  0ofval  29158  hashxpe  31136  esumcvg  32063  sxbrsigalem0  32247  sxbrsigalem3  32248  sxbrsigalem2  32262  ofcccat  32531  lpadval  32665  lpadlem3  32667  mexval2  33474  xpord2pred  33801  xpord3pred  33807  naddcllem  33840  csbfinxpg  35568  poimirlem1  35787  poimirlem2  35788  poimirlem3  35789  poimirlem4  35790  poimirlem5  35791  poimirlem6  35792  poimirlem7  35793  poimirlem8  35794  poimirlem10  35796  poimirlem11  35797  poimirlem12  35798  poimirlem15  35801  poimirlem16  35802  poimirlem17  35803  poimirlem18  35804  poimirlem19  35805  poimirlem20  35806  poimirlem21  35807  poimirlem22  35808  poimirlem23  35809  poimirlem24  35810  poimirlem26  35812  poimirlem27  35813  poimirlem28  35814  poimirlem32  35818  sdclem1  35910  ismrer1  36005  ldualset  37146  dibval  39163  dibval3N  39167  dib0  39185  dihwN  39310  hdmap1fval  39817  fsuppssind  40289  mzpclval  40554  mendval  41015  prstcval  46356  prstchomval  46366