Theorem xpeq1d 5680

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

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

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 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-opab 5168  df-xp 5657

This theorem is used by:  csbres  5973  xpssres  6009  curry1  8104  fparlem3  8114  fparlem4  8115  xpord2pred  8146  xpord3pred  8153  naddcllem  8669  ixpsnf1o  8950  dfac5lem3  10185  dfac5lem4  10186  hashxplem  14558  repsw1  14914  subgga  19494  gasubg  19496  sylow2blem2  19815  psrval  22203  mpfrcl  22374  evlsval  22375  mamufval  22687  mat1dimscm  22770  mdetunilem3  22909  mdetunilem4  22910  mdetunilem9  22915  txindislem  23932  txtube  23939  txcmplem1  23940  txhaus  23946  xkoinjcn  23986  pt1hmeo  24105  tsmsxplem1  24452  tsmsxplem2  24453  cnmpopc  25229  dchrval  27543  axlowdimlem15  29516  axlowdim  29521  0ofval  31371  fconst7v  33196  hashxpe  33381  erlval  33801  fracbas  33849  esumcvg  34700  sxbrsigalem0  34886  sxbrsigalem3  34887  sxbrsigalem2  34901  ofcccat  35158  lpadval  35291  lpadlem3  35293  mexval2  36237  csbfinxpg  38279  poimirlem1  38507  poimirlem2  38508  poimirlem3  38509  poimirlem4  38510  poimirlem5  38511  poimirlem6  38512  poimirlem7  38513  poimirlem8  38514  poimirlem10  38516  poimirlem11  38517  poimirlem12  38518  poimirlem15  38521  poimirlem16  38522  poimirlem17  38523  poimirlem18  38524  poimirlem19  38525  poimirlem20  38526  poimirlem21  38527  poimirlem22  38528  poimirlem23  38529  poimirlem24  38530  poimirlem26  38532  poimirlem27  38533  poimirlem28  38534  poimirlem32  38538  sdclem1  38645  ismrer1  38740  ldualset  40150  dibval  42167  dibval3N  42171  dib0  42189  dihwN  42314  hdmap1fval  42821  fsuppssind  43583  mzpclval  43689  mendval  44139  dmrnxp  49891  diag1f1olem  50585  diag2f1olem  50588  prstcval  50603  prstchomval  50611