Theorem xpeq1d 5695

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   × cxp 5664

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-opab 5179  df-xp 5672

This theorem is used by:  csbres  5986  xpssres  6022  curry1  8108  fparlem3  8118  fparlem4  8119  xpord2pred  8150  xpord3pred  8157  naddcllem  8671  ixpsnf1o  8945  dfac5lem3  10128  dfac5lem4  10129  hashxplem  14490  repsw1  14846  subgga  19401  gasubg  19403  sylow2blem2  19722  psrval  22102  mpfrcl  22273  evlsval  22274  mamufval  22586  mat1dimscm  22669  mdetunilem3  22808  mdetunilem4  22809  mdetunilem9  22814  txindislem  23827  txtube  23834  txcmplem1  23835  txhaus  23841  xkoinjcn  23881  pt1hmeo  24000  tsmsxplem1  24347  tsmsxplem2  24348  cnmpopc  25124  dchrval  27435  axlowdimlem15  29343  axlowdim  29348  0ofval  31176  fconst7v  33002  hashxpe  33189  erlval  33609  fracbas  33657  esumcvg  34507  sxbrsigalem0  34693  sxbrsigalem3  34694  sxbrsigalem2  34708  ofcccat  34965  lpadval  35098  lpadlem3  35100  mexval2  36016  csbfinxpg  38075  poimirlem1  38313  poimirlem2  38314  poimirlem3  38315  poimirlem4  38316  poimirlem5  38317  poimirlem6  38318  poimirlem7  38319  poimirlem8  38320  poimirlem10  38322  poimirlem11  38323  poimirlem12  38324  poimirlem15  38327  poimirlem16  38328  poimirlem17  38329  poimirlem18  38330  poimirlem19  38331  poimirlem20  38332  poimirlem21  38333  poimirlem22  38334  poimirlem23  38335  poimirlem24  38336  poimirlem26  38338  poimirlem27  38339  poimirlem28  38340  poimirlem32  38344  sdclem1  38435  ismrer1  38530  ldualset  39940  dibval  41957  dibval3N  41961  dib0  41979  dihwN  42104  hdmap1fval  42611  fsuppssind  43366  mzpclval  43497  mendval  43947  dmrnxp  49656  diag1f1olem  50352  diag2f1olem  50355  prstcval  50370  prstchomval  50378