Theorem xpeq1d 5706

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

Syntax hints:   → wi 4   = wceq 1542   × cxp 5675

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-opab 5212  df-xp 5683

This theorem is referenced by:  csbres  5985  xpssres  6019  curry1  8090  fparlem3  8100  fparlem4  8101  xpord2pred  8131  xpord3pred  8138  naddcllem  8675  ixpsnf1o  8932  xpfiOLD  9318  dfac5lem3  10120  dfac5lem4  10121  hashxplem  14393  repsw1  14733  subgga  19164  gasubg  19166  sylow2blem2  19489  psrval  21468  mpfrcl  21648  evlsval  21649  mamufval  21887  mat1dimscm  21977  mdetunilem3  22116  mdetunilem4  22117  mdetunilem9  22122  txindislem  23137  txtube  23144  txcmplem1  23145  txhaus  23151  xkoinjcn  23191  pt1hmeo  23310  tsmsxplem1  23657  tsmsxplem2  23658  cnmpopc  24444  dchrval  26737  axlowdimlem15  28214  axlowdim  28219  0ofval  30040  hashxpe  32019  esumcvg  33084  sxbrsigalem0  33270  sxbrsigalem3  33271  sxbrsigalem2  33285  ofcccat  33554  lpadval  33688  lpadlem3  33690  mexval2  34494  csbfinxpg  36269  poimirlem1  36489  poimirlem2  36490  poimirlem3  36491  poimirlem4  36492  poimirlem5  36493  poimirlem6  36494  poimirlem7  36495  poimirlem8  36496  poimirlem10  36498  poimirlem11  36499  poimirlem12  36500  poimirlem15  36503  poimirlem16  36504  poimirlem17  36505  poimirlem18  36506  poimirlem19  36507  poimirlem20  36508  poimirlem21  36509  poimirlem22  36510  poimirlem23  36511  poimirlem24  36512  poimirlem26  36514  poimirlem27  36515  poimirlem28  36516  poimirlem32  36520  sdclem1  36611  ismrer1  36706  ldualset  37995  dibval  40013  dibval3N  40017  dib0  40035  dihwN  40160  hdmap1fval  40667  fsuppssind  41165  mzpclval  41463  mendval  41925  prstcval  47684  prstchomval  47694