Theorem xpeq1d 5670

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-opab 5173  df-xp 5647

This theorem is referenced by:  csbres  5956  xpssres  5992  curry1  8086  fparlem3  8096  fparlem4  8097  xpord2pred  8127  xpord3pred  8134  naddcllem  8643  ixpsnf1o  8914  xpfiOLD  9277  dfac5lem3  10085  dfac5lem4  10086  dfac5lem4OLD  10088  hashxplem  14405  repsw1  14755  subgga  19239  gasubg  19241  sylow2blem2  19558  psrval  21831  mpfrcl  21999  evlsval  22000  mamufval  22286  mat1dimscm  22369  mdetunilem3  22508  mdetunilem4  22509  mdetunilem9  22514  txindislem  23527  txtube  23534  txcmplem1  23535  txhaus  23541  xkoinjcn  23581  pt1hmeo  23700  tsmsxplem1  24047  tsmsxplem2  24048  cnmpopc  24829  dchrval  27152  axlowdimlem15  28890  axlowdim  28895  0ofval  30723  hashxpe  32739  erlval  33216  fracbas  33262  esumcvg  34083  sxbrsigalem0  34269  sxbrsigalem3  34270  sxbrsigalem2  34284  ofcccat  34541  lpadval  34674  lpadlem3  34676  mexval2  35497  csbfinxpg  37383  poimirlem1  37622  poimirlem2  37623  poimirlem3  37624  poimirlem4  37625  poimirlem5  37626  poimirlem6  37627  poimirlem7  37628  poimirlem8  37629  poimirlem10  37631  poimirlem11  37632  poimirlem12  37633  poimirlem15  37636  poimirlem16  37637  poimirlem17  37638  poimirlem18  37639  poimirlem19  37640  poimirlem20  37641  poimirlem21  37642  poimirlem22  37643  poimirlem23  37644  poimirlem24  37645  poimirlem26  37647  poimirlem27  37648  poimirlem28  37649  poimirlem32  37653  sdclem1  37744  ismrer1  37839  ldualset  39125  dibval  41143  dibval3N  41147  dib0  41165  dihwN  41290  hdmap1fval  41797  fsuppssind  42588  mzpclval  42720  mendval  43175  dmrnxp  48829  diag1f1olem  49526  diag2f1olem  49529  prstcval  49544  prstchomval  49552