Theorem xpeq1d 5729

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

Syntax hints:   → wi 4   = wceq 1537   × cxp 5698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-opab 5229  df-xp 5706

This theorem is referenced by:  csbres  6012  xpssres  6047  curry1  8145  fparlem3  8155  fparlem4  8156  xpord2pred  8186  xpord3pred  8193  naddcllem  8732  ixpsnf1o  8996  xpfiOLD  9387  dfac5lem3  10194  dfac5lem4  10195  dfac5lem4OLD  10197  hashxplem  14482  repsw1  14831  subgga  19340  gasubg  19342  sylow2blem2  19663  psrval  21958  mpfrcl  22132  evlsval  22133  mamufval  22417  mat1dimscm  22502  mdetunilem3  22641  mdetunilem4  22642  mdetunilem9  22647  txindislem  23662  txtube  23669  txcmplem1  23670  txhaus  23676  xkoinjcn  23716  pt1hmeo  23835  tsmsxplem1  24182  tsmsxplem2  24183  cnmpopc  24974  dchrval  27296  axlowdimlem15  28989  axlowdim  28994  0ofval  30819  hashxpe  32814  erlval  33230  fracbas  33272  esumcvg  34050  sxbrsigalem0  34236  sxbrsigalem3  34237  sxbrsigalem2  34251  ofcccat  34520  lpadval  34653  lpadlem3  34655  mexval2  35471  csbfinxpg  37354  poimirlem1  37581  poimirlem2  37582  poimirlem3  37583  poimirlem4  37584  poimirlem5  37585  poimirlem6  37586  poimirlem7  37587  poimirlem8  37588  poimirlem10  37590  poimirlem11  37591  poimirlem12  37592  poimirlem15  37595  poimirlem16  37596  poimirlem17  37597  poimirlem18  37598  poimirlem19  37599  poimirlem20  37600  poimirlem21  37601  poimirlem22  37602  poimirlem23  37603  poimirlem24  37604  poimirlem26  37606  poimirlem27  37607  poimirlem28  37608  poimirlem32  37612  sdclem1  37703  ismrer1  37798  ldualset  39081  dibval  41099  dibval3N  41103  dib0  41121  dihwN  41246  hdmap1fval  41753  fsuppssind  42548  mzpclval  42681  mendval  43140  prstcval  48731  prstchomval  48741