Theorem xpeq1d 5472

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

Syntax hints:   → wi 4   = wceq 1522   × cxp 5441

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-opab 5025  df-xp 5449

This theorem is referenced by:  csbres  5737  xpssres  5770  curry1  7655  fparlem3  7665  fparlem4  7666  ixpsnf1o  8350  xpfi  8635  dfac5lem3  9397  dfac5lem4  9398  hashxplem  13642  repsw1  13981  subgga  18171  gasubg  18173  sylow2blem2  18476  psrval  19830  mpfrcl  19985  evlsval  19986  mamufval  20678  mat1dimscm  20768  mdetunilem3  20907  mdetunilem4  20908  mdetunilem9  20913  txindislem  21925  txtube  21932  txcmplem1  21933  txhaus  21939  xkoinjcn  21979  pt1hmeo  22098  tsmsxplem1  22444  tsmsxplem2  22445  cnmpopc  23215  dchrval  25492  axlowdimlem15  26425  axlowdim  26430  0ofval  28255  hashxpe  30213  esumcvg  30962  sxbrsigalem0  31146  sxbrsigalem3  31147  sxbrsigalem2  31161  ofcccat  31430  lpadval  31564  lpadlem3  31566  mexval2  32358  csbfinxpg  34200  poimirlem1  34424  poimirlem2  34425  poimirlem3  34426  poimirlem4  34427  poimirlem5  34428  poimirlem6  34429  poimirlem7  34430  poimirlem8  34431  poimirlem10  34433  poimirlem11  34434  poimirlem12  34435  poimirlem15  34438  poimirlem16  34439  poimirlem17  34440  poimirlem18  34441  poimirlem19  34442  poimirlem20  34443  poimirlem21  34444  poimirlem22  34445  poimirlem23  34446  poimirlem24  34447  poimirlem26  34449  poimirlem27  34450  poimirlem28  34451  poimirlem32  34455  sdclem1  34550  ismrer1  34648  ldualset  35792  dibval  37809  dibval3N  37813  dib0  37831  dihwN  37956  hdmap1fval  38463  mzpclval  38807  mendval  39268