Theorem xpeq1d 5701

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

Syntax hints:   → wi 4   = wceq 1534   × cxp 5670

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-opab 5206  df-xp 5678

This theorem is referenced by:  csbres  5982  xpssres  6017  curry1  8107  fparlem3  8117  fparlem4  8118  xpord2pred  8148  xpord3pred  8155  naddcllem  8695  ixpsnf1o  8956  xpfiOLD  9351  dfac5lem3  10158  dfac5lem4  10159  hashxplem  14442  repsw1  14783  subgga  19287  gasubg  19289  sylow2blem2  19612  psrval  21905  mpfrcl  22093  evlsval  22094  mamufval  22377  mat1dimscm  22462  mdetunilem3  22601  mdetunilem4  22602  mdetunilem9  22607  txindislem  23622  txtube  23629  txcmplem1  23630  txhaus  23636  xkoinjcn  23676  pt1hmeo  23795  tsmsxplem1  24142  tsmsxplem2  24143  cnmpopc  24934  dchrval  27257  axlowdimlem15  28884  axlowdim  28889  0ofval  30714  hashxpe  32711  erlval  33115  fracbas  33157  esumcvg  33929  sxbrsigalem0  34115  sxbrsigalem3  34116  sxbrsigalem2  34130  ofcccat  34399  lpadval  34532  lpadlem3  34534  mexval2  35341  csbfinxpg  37105  poimirlem1  37332  poimirlem2  37333  poimirlem3  37334  poimirlem4  37335  poimirlem5  37336  poimirlem6  37337  poimirlem7  37338  poimirlem8  37339  poimirlem10  37341  poimirlem11  37342  poimirlem12  37343  poimirlem15  37346  poimirlem16  37347  poimirlem17  37348  poimirlem18  37349  poimirlem19  37350  poimirlem20  37351  poimirlem21  37352  poimirlem22  37353  poimirlem23  37354  poimirlem24  37355  poimirlem26  37357  poimirlem27  37358  poimirlem28  37359  poimirlem32  37363  sdclem1  37454  ismrer1  37549  ldualset  38833  dibval  40851  dibval3N  40855  dib0  40873  dihwN  40998  hdmap1fval  41505  fsuppssind  42280  mzpclval  42416  mendval  42878  prstcval  48418  prstchomval  48428