Theorem xpeq1d 5138

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

Syntax hints:   → wi 4   = wceq 1483   × cxp 5112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-opab 4713  df-xp 5120

This theorem is referenced by:  csbres  5399  xpssres  5434  curry1  7269  fparlem3  7279  fparlem4  7280  ixpsnf1o  7948  xpfi  8231  dfac5lem3  8948  dfac5lem4  8949  cdaassen  9004  hashxplem  13220  repsw1  13530  subgga  17733  gasubg  17735  sylow2blem2  18036  psrval  19362  mpfrcl  19518  evlsval  19519  mamufval  20191  mat1dimscm  20281  mdetunilem3  20420  mdetunilem4  20421  mdetunilem9  20426  txindislem  21436  txtube  21443  txcmplem1  21444  txhaus  21450  xkoinjcn  21490  pt1hmeo  21609  tsmsxplem1  21956  tsmsxplem2  21957  cnmpt2pc  22727  dchrval  24959  axlowdimlem15  25836  axlowdim  25841  0ofval  27642  esumcvg  30148  sxbrsigalem0  30333  sxbrsigalem3  30334  sxbrsigalem2  30348  ofcccat  30620  mexval2  31400  csbfinxpg  33225  poimirlem1  33410  poimirlem2  33411  poimirlem3  33412  poimirlem4  33413  poimirlem5  33414  poimirlem6  33415  poimirlem7  33416  poimirlem8  33417  poimirlem10  33419  poimirlem11  33420  poimirlem12  33421  poimirlem15  33424  poimirlem16  33425  poimirlem17  33426  poimirlem18  33427  poimirlem19  33428  poimirlem20  33429  poimirlem21  33430  poimirlem22  33431  poimirlem23  33432  poimirlem24  33433  poimirlem26  33435  poimirlem27  33436  poimirlem28  33437  poimirlem32  33441  sdclem1  33539  ismrer1  33637  ldualset  34412  dibval  36431  dibval3N  36435  dib0  36453  dihwN  36578  hdmap1fval  37086  mzpclval  37288  mendval  37753