Theorem xpeq1d 5688

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

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

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 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-opab 5172  df-xp 5665

This theorem is used by:  csbres  5979  xpssres  6015  curry1  8105  fparlem3  8115  fparlem4  8116  xpord2pred  8147  xpord3pred  8154  naddcllem  8668  ixpsnf1o  8949  dfac5lem3  10132  dfac5lem4  10133  hashxplem  14502  repsw1  14858  subgga  19433  gasubg  19435  sylow2blem2  19754  psrval  22136  mpfrcl  22307  evlsval  22308  mamufval  22620  mat1dimscm  22703  mdetunilem3  22842  mdetunilem4  22843  mdetunilem9  22848  txindislem  23865  txtube  23872  txcmplem1  23873  txhaus  23879  xkoinjcn  23919  pt1hmeo  24038  tsmsxplem1  24385  tsmsxplem2  24386  cnmpopc  25162  dchrval  27478  axlowdimlem15  29421  axlowdim  29426  0ofval  31276  fconst7v  33101  hashxpe  33286  erlval  33706  fracbas  33754  esumcvg  34604  sxbrsigalem0  34790  sxbrsigalem3  34791  sxbrsigalem2  34805  ofcccat  35062  lpadval  35195  lpadlem3  35197  mexval2  36090  csbfinxpg  38150  poimirlem1  38378  poimirlem2  38379  poimirlem3  38380  poimirlem4  38381  poimirlem5  38382  poimirlem6  38383  poimirlem7  38384  poimirlem8  38385  poimirlem10  38387  poimirlem11  38388  poimirlem12  38389  poimirlem15  38392  poimirlem16  38393  poimirlem17  38394  poimirlem18  38395  poimirlem19  38396  poimirlem20  38397  poimirlem21  38398  poimirlem22  38399  poimirlem23  38400  poimirlem24  38401  poimirlem26  38403  poimirlem27  38404  poimirlem28  38405  poimirlem32  38409  sdclem1  38501  ismrer1  38596  ldualset  40006  dibval  42023  dibval3N  42027  dib0  42045  dihwN  42170  hdmap1fval  42677  fsuppssind  43447  mzpclval  43578  mendval  44028  dmrnxp  49773  diag1f1olem  50467  diag2f1olem  50470  prstcval  50485  prstchomval  50493