Theorem xpeq1d 5062

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

Syntax hints:   → wi 4   = wceq 1475   × cxp 5036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-opab 4644  df-xp 5044

This theorem is referenced by:  csbres  5320  xpssres  5354  curry1  7156  fparlem3  7166  fparlem4  7167  ixpsnf1o  7834  xpfi  8116  dfac5lem3  8831  dfac5lem4  8832  cdaassen  8887  hashxplem  13080  repsw1  13381  subgga  17556  gasubg  17558  sylow2blem2  17859  psrval  19183  mpfrcl  19339  evlsval  19340  mamufval  20010  mat1dimscm  20100  mdetunilem3  20239  mdetunilem4  20240  mdetunilem9  20245  txindislem  21246  txtube  21253  txcmplem1  21254  txhaus  21260  xkoinjcn  21300  pt1hmeo  21419  tsmsxplem1  21766  tsmsxplem2  21767  cnmpt2pc  22535  dchrval  24759  axlowdimlem15  25636  axlowdim  25641  0ofval  27026  esumcvg  29475  sxbrsigalem0  29660  sxbrsigalem3  29661  sxbrsigalem2  29675  ofcccat  29946  mexval2  30654  csbfinxpg  32401  poimirlem1  32580  poimirlem2  32581  poimirlem3  32582  poimirlem4  32583  poimirlem5  32584  poimirlem6  32585  poimirlem7  32586  poimirlem8  32587  poimirlem10  32589  poimirlem11  32590  poimirlem12  32591  poimirlem15  32594  poimirlem16  32595  poimirlem17  32596  poimirlem18  32597  poimirlem19  32598  poimirlem20  32599  poimirlem21  32600  poimirlem22  32601  poimirlem23  32602  poimirlem24  32603  poimirlem26  32605  poimirlem27  32606  poimirlem28  32607  poimirlem32  32611  sdclem1  32709  ismrer1  32807  ldualset  33430  dibval  35449  dibval3N  35453  dib0  35471  dihwN  35596  hdmap1fval  36104  mzpclval  36306  mendval  36772