Theorem xpeq1d 5714

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-opab 5206  df-xp 5691

This theorem is referenced by:  csbres  6000  xpssres  6036  curry1  8129  fparlem3  8139  fparlem4  8140  xpord2pred  8170  xpord3pred  8177  naddcllem  8714  ixpsnf1o  8978  xpfiOLD  9359  dfac5lem3  10165  dfac5lem4  10166  dfac5lem4OLD  10168  hashxplem  14472  repsw1  14821  subgga  19318  gasubg  19320  sylow2blem2  19639  psrval  21935  mpfrcl  22109  evlsval  22110  mamufval  22396  mat1dimscm  22481  mdetunilem3  22620  mdetunilem4  22621  mdetunilem9  22626  txindislem  23641  txtube  23648  txcmplem1  23649  txhaus  23655  xkoinjcn  23695  pt1hmeo  23814  tsmsxplem1  24161  tsmsxplem2  24162  cnmpopc  24955  dchrval  27278  axlowdimlem15  28971  axlowdim  28976  0ofval  30806  hashxpe  32811  erlval  33262  fracbas  33307  esumcvg  34087  sxbrsigalem0  34273  sxbrsigalem3  34274  sxbrsigalem2  34288  ofcccat  34558  lpadval  34691  lpadlem3  34693  mexval2  35508  csbfinxpg  37389  poimirlem1  37628  poimirlem2  37629  poimirlem3  37630  poimirlem4  37631  poimirlem5  37632  poimirlem6  37633  poimirlem7  37634  poimirlem8  37635  poimirlem10  37637  poimirlem11  37638  poimirlem12  37639  poimirlem15  37642  poimirlem16  37643  poimirlem17  37644  poimirlem18  37645  poimirlem19  37646  poimirlem20  37647  poimirlem21  37648  poimirlem22  37649  poimirlem23  37650  poimirlem24  37651  poimirlem26  37653  poimirlem27  37654  poimirlem28  37655  poimirlem32  37659  sdclem1  37750  ismrer1  37845  ldualset  39126  dibval  41144  dibval3N  41148  dib0  41166  dihwN  41291  hdmap1fval  41798  fsuppssind  42603  mzpclval  42736  mendval  43191  prstcval  49153  prstchomval  49163