Theorem xpeq1d 5580

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

Syntax hints:   → wi 4   = wceq 1543   × cxp 5549

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-opab 5116  df-xp 5557

This theorem is referenced by:  csbres  5854  xpssres  5888  curry1  7872  fparlem3  7882  fparlem4  7883  ixpsnf1o  8619  xpfi  8942  dfac5lem3  9739  dfac5lem4  9740  hashxplem  14000  repsw1  14348  subgga  18694  gasubg  18696  sylow2blem2  19010  psrval  20874  mpfrcl  21045  evlsval  21046  mamufval  21284  mat1dimscm  21372  mdetunilem3  21511  mdetunilem4  21512  mdetunilem9  21517  txindislem  22530  txtube  22537  txcmplem1  22538  txhaus  22544  xkoinjcn  22584  pt1hmeo  22703  tsmsxplem1  23050  tsmsxplem2  23051  cnmpopc  23825  dchrval  26115  axlowdimlem15  27047  axlowdim  27052  0ofval  28868  hashxpe  30847  esumcvg  31766  sxbrsigalem0  31950  sxbrsigalem3  31951  sxbrsigalem2  31965  ofcccat  32234  lpadval  32368  lpadlem3  32370  mexval2  33178  xpord2pred  33529  xpord3pred  33535  naddcllem  33568  csbfinxpg  35296  poimirlem1  35515  poimirlem2  35516  poimirlem3  35517  poimirlem4  35518  poimirlem5  35519  poimirlem6  35520  poimirlem7  35521  poimirlem8  35522  poimirlem10  35524  poimirlem11  35525  poimirlem12  35526  poimirlem15  35529  poimirlem16  35530  poimirlem17  35531  poimirlem18  35532  poimirlem19  35533  poimirlem20  35534  poimirlem21  35535  poimirlem22  35536  poimirlem23  35537  poimirlem24  35538  poimirlem26  35540  poimirlem27  35541  poimirlem28  35542  poimirlem32  35546  sdclem1  35638  ismrer1  35733  ldualset  36876  dibval  38893  dibval3N  38897  dib0  38915  dihwN  39040  hdmap1fval  39547  fsuppssind  39992  mzpclval  40250  mendval  40711  prstcval  46018  prstchomval  46026