Theorem xpeq1d 5717

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

Syntax hints:   → wi 4   = wceq 1536   × cxp 5686

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-opab 5210  df-xp 5694

This theorem is referenced by:  csbres  6002  xpssres  6037  curry1  8127  fparlem3  8137  fparlem4  8138  xpord2pred  8168  xpord3pred  8175  naddcllem  8712  ixpsnf1o  8976  xpfiOLD  9356  dfac5lem3  10162  dfac5lem4  10163  dfac5lem4OLD  10165  hashxplem  14468  repsw1  14817  subgga  19330  gasubg  19332  sylow2blem2  19653  psrval  21952  mpfrcl  22126  evlsval  22127  mamufval  22411  mat1dimscm  22496  mdetunilem3  22635  mdetunilem4  22636  mdetunilem9  22641  txindislem  23656  txtube  23663  txcmplem1  23664  txhaus  23670  xkoinjcn  23710  pt1hmeo  23829  tsmsxplem1  24176  tsmsxplem2  24177  cnmpopc  24968  dchrval  27292  axlowdimlem15  28985  axlowdim  28990  0ofval  30815  hashxpe  32816  erlval  33244  fracbas  33286  esumcvg  34066  sxbrsigalem0  34252  sxbrsigalem3  34253  sxbrsigalem2  34267  ofcccat  34536  lpadval  34669  lpadlem3  34671  mexval2  35487  csbfinxpg  37370  poimirlem1  37607  poimirlem2  37608  poimirlem3  37609  poimirlem4  37610  poimirlem5  37611  poimirlem6  37612  poimirlem7  37613  poimirlem8  37614  poimirlem10  37616  poimirlem11  37617  poimirlem12  37618  poimirlem15  37621  poimirlem16  37622  poimirlem17  37623  poimirlem18  37624  poimirlem19  37625  poimirlem20  37626  poimirlem21  37627  poimirlem22  37628  poimirlem23  37629  poimirlem24  37630  poimirlem26  37632  poimirlem27  37633  poimirlem28  37634  poimirlem32  37638  sdclem1  37729  ismrer1  37824  ldualset  39106  dibval  41124  dibval3N  41128  dib0  41146  dihwN  41271  hdmap1fval  41778  fsuppssind  42579  mzpclval  42712  mendval  43167  prstcval  48864  prstchomval  48874