Theorem xpeq1d 5052

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

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

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 4639  df-xp 5034

This theorem is referenced by:  csbres  5307  xpssres  5341  curry1  7134  fparlem3  7144  fparlem4  7145  ixpsnf1o  7812  xpfi  8094  dfac5lem3  8809  dfac5lem4  8810  cdaassen  8865  hashxplem  13035  repsw1  13330  subgga  17505  gasubg  17507  sylow2blem2  17808  psrval  19132  mpfrcl  19288  evlsval  19289  mamufval  19958  mat1dimscm  20048  mdetunilem3  20187  mdetunilem4  20188  mdetunilem9  20193  txindislem  21194  txtube  21201  txcmplem1  21202  txhaus  21208  xkoinjcn  21248  pt1hmeo  21367  tsmsxplem1  21714  tsmsxplem2  21715  cnmpt2pc  22483  dchrval  24704  axlowdimlem15  25582  axlowdim  25587  0ofval  26820  esumcvg  29269  sxbrsigalem0  29454  sxbrsigalem3  29455  sxbrsigalem2  29469  ofcccat  29740  mexval2  30448  csbfinxpg  32195  poimirlem1  32374  poimirlem2  32375  poimirlem3  32376  poimirlem4  32377  poimirlem5  32378  poimirlem6  32379  poimirlem7  32380  poimirlem8  32381  poimirlem10  32383  poimirlem11  32384  poimirlem12  32385  poimirlem15  32388  poimirlem16  32389  poimirlem17  32390  poimirlem18  32391  poimirlem19  32392  poimirlem20  32393  poimirlem21  32394  poimirlem22  32395  poimirlem23  32396  poimirlem24  32397  poimirlem26  32399  poimirlem27  32400  poimirlem28  32401  poimirlem32  32405  sdclem1  32503  ismrer1  32601  ldualset  33224  dibval  35243  dibval3N  35247  dib0  35265  dihwN  35390  hdmap1fval  35898  mzpclval  36100  mendval  36566