Theorem xpeq1d 5637

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

Syntax hints:   → wi 4   = wceq 1540   × cxp 5606

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1781  df-sb 2067  df-clab 2715  df-cleq 2729  df-clel 2815  df-opab 5150  df-xp 5614

This theorem is referenced by:  csbres  5914  xpssres  5948  curry1  7991  fparlem3  8001  fparlem4  8002  ixpsnf1o  8776  xpfiOLD  9162  dfac5lem3  9961  dfac5lem4  9962  hashxplem  14227  repsw1  14575  subgga  18982  gasubg  18984  sylow2blem2  19302  psrval  21201  mpfrcl  21378  evlsval  21379  mamufval  21617  mat1dimscm  21707  mdetunilem3  21846  mdetunilem4  21847  mdetunilem9  21852  txindislem  22867  txtube  22874  txcmplem1  22875  txhaus  22881  xkoinjcn  22921  pt1hmeo  23040  tsmsxplem1  23387  tsmsxplem2  23388  cnmpopc  24174  dchrval  26465  axlowdimlem15  27460  axlowdim  27465  0ofval  29285  hashxpe  31262  esumcvg  32194  sxbrsigalem0  32378  sxbrsigalem3  32379  sxbrsigalem2  32393  ofcccat  32662  lpadval  32796  lpadlem3  32798  mexval2  33604  xpord2pred  33922  xpord3pred  33928  naddcllem  33958  csbfinxpg  35631  poimirlem1  35850  poimirlem2  35851  poimirlem3  35852  poimirlem4  35853  poimirlem5  35854  poimirlem6  35855  poimirlem7  35856  poimirlem8  35857  poimirlem10  35859  poimirlem11  35860  poimirlem12  35861  poimirlem15  35864  poimirlem16  35865  poimirlem17  35866  poimirlem18  35867  poimirlem19  35868  poimirlem20  35869  poimirlem21  35870  poimirlem22  35871  poimirlem23  35872  poimirlem24  35873  poimirlem26  35875  poimirlem27  35876  poimirlem28  35877  poimirlem32  35881  sdclem1  35973  ismrer1  36068  ldualset  37359  dibval  39377  dibval3N  39381  dib0  39399  dihwN  39524  hdmap1fval  40031  fsuppssind  40498  mzpclval  40763  mendval  41225  prstcval  46610  prstchomval  46620