Theorem xpeq1d 5683

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

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

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-opab 5182  df-xp 5660

This theorem is referenced by:  csbres  5969  xpssres  6005  curry1  8101  fparlem3  8111  fparlem4  8112  xpord2pred  8142  xpord3pred  8149  naddcllem  8686  ixpsnf1o  8950  xpfiOLD  9329  dfac5lem3  10137  dfac5lem4  10138  dfac5lem4OLD  10140  hashxplem  14449  repsw1  14799  subgga  19281  gasubg  19283  sylow2blem2  19600  psrval  21873  mpfrcl  22041  evlsval  22042  mamufval  22328  mat1dimscm  22411  mdetunilem3  22550  mdetunilem4  22551  mdetunilem9  22556  txindislem  23569  txtube  23576  txcmplem1  23577  txhaus  23583  xkoinjcn  23623  pt1hmeo  23742  tsmsxplem1  24089  tsmsxplem2  24090  cnmpopc  24871  dchrval  27195  axlowdimlem15  28881  axlowdim  28886  0ofval  30714  hashxpe  32732  erlval  33199  fracbas  33245  esumcvg  34063  sxbrsigalem0  34249  sxbrsigalem3  34250  sxbrsigalem2  34264  ofcccat  34521  lpadval  34654  lpadlem3  34656  mexval2  35471  csbfinxpg  37352  poimirlem1  37591  poimirlem2  37592  poimirlem3  37593  poimirlem4  37594  poimirlem5  37595  poimirlem6  37596  poimirlem7  37597  poimirlem8  37598  poimirlem10  37600  poimirlem11  37601  poimirlem12  37602  poimirlem15  37605  poimirlem16  37606  poimirlem17  37607  poimirlem18  37608  poimirlem19  37609  poimirlem20  37610  poimirlem21  37611  poimirlem22  37612  poimirlem23  37613  poimirlem24  37614  poimirlem26  37616  poimirlem27  37617  poimirlem28  37618  poimirlem32  37622  sdclem1  37713  ismrer1  37808  ldualset  39089  dibval  41107  dibval3N  41111  dib0  41129  dihwN  41254  hdmap1fval  41761  fsuppssind  42563  mzpclval  42695  mendval  43150  dmrnxp  48763  diag1f1olem  49366  diag2f1olem  49369  prstcval  49376  prstchomval  49384