Theorem xpeq1d 5692

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

Syntax hints:   → wi 4   = wceq 1570   × cxp 5661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-opab 5175  df-xp 5669

This theorem is referenced by:  csbres  5983  xpssres  6019  curry1  8100  fparlem3  8110  fparlem4  8111  xpord2pred  8142  xpord3pred  8149  naddcllem  8663  ixpsnf1o  8937  dfac5lem3  10110  dfac5lem4  10111  hashxplem  14472  repsw1  14822  subgga  19371  gasubg  19373  sylow2blem2  19692  psrval  22046  mpfrcl  22217  evlsval  22218  mamufval  22530  mat1dimscm  22613  mdetunilem3  22752  mdetunilem4  22753  mdetunilem9  22758  txindislem  23771  txtube  23778  txcmplem1  23779  txhaus  23785  xkoinjcn  23825  pt1hmeo  23944  tsmsxplem1  24291  tsmsxplem2  24292  cnmpopc  25068  dchrval  27379  axlowdimlem15  29287  axlowdim  29292  0ofval  31120  fconst7v  32946  hashxpe  33133  erlval  33559  fracbas  33607  esumcvg  34457  sxbrsigalem0  34642  sxbrsigalem3  34643  sxbrsigalem2  34657  ofcccat  34914  lpadval  35047  lpadlem3  35049  mexval2  35976  csbfinxpg  38015  poimirlem1  38253  poimirlem2  38254  poimirlem3  38255  poimirlem4  38256  poimirlem5  38257  poimirlem6  38258  poimirlem7  38259  poimirlem8  38260  poimirlem10  38262  poimirlem11  38263  poimirlem12  38264  poimirlem15  38267  poimirlem16  38268  poimirlem17  38269  poimirlem18  38270  poimirlem19  38271  poimirlem20  38272  poimirlem21  38273  poimirlem22  38274  poimirlem23  38275  poimirlem24  38276  poimirlem26  38278  poimirlem27  38279  poimirlem28  38280  poimirlem32  38284  sdclem1  38375  ismrer1  38470  ldualset  39880  dibval  41897  dibval3N  41901  dib0  41919  dihwN  42044  hdmap1fval  42551  fsuppssind  43308  mzpclval  43439  mendval  43889  dmrnxp  49598  diag1f1olem  50294  diag2f1olem  50297  prstcval  50312  prstchomval  50320