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  28245  axlowdim  28250  0ofval  30071  hashxpe  32050  esumcvg  33115  sxbrsigalem0  33301  sxbrsigalem3  33302  sxbrsigalem2  33316  ofcccat  33585  lpadval  33719  lpadlem3  33721  mexval2  34525  csbfinxpg  36317  poimirlem1  36537  poimirlem2  36538  poimirlem3  36539  poimirlem4  36540  poimirlem5  36541  poimirlem6  36542  poimirlem7  36543  poimirlem8  36544  poimirlem10  36546  poimirlem11  36547  poimirlem12  36548  poimirlem15  36551  poimirlem16  36552  poimirlem17  36553  poimirlem18  36554  poimirlem19  36555  poimirlem20  36556  poimirlem21  36557  poimirlem22  36558  poimirlem23  36559  poimirlem24  36560  poimirlem26  36562  poimirlem27  36563  poimirlem28  36564  poimirlem32  36568  sdclem1  36659  ismrer1  36754  ldualset  38043  dibval  40061  dibval3N  40065  dib0  40083  dihwN  40208  hdmap1fval  40715  fsuppssind  41213  mzpclval  41511  mendval  41973  prstcval  47732  prstchomval  47742