Theorem xpeq1d 5680

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

Syntax hints:   → wi 4   = wceq 1563   × cxp 5649

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-opab 5167  df-xp 5657

This theorem is referenced by:  csbres  5971  xpssres  6007  curry1  8087  fparlem3  8097  fparlem4  8098  xpord2pred  8129  xpord3pred  8136  naddcllem  8650  ixpsnf1o  8924  dfac5lem3  10097  dfac5lem4  10098  hashxplem  14458  repsw1  14808  subgga  19358  gasubg  19360  sylow2blem2  19679  psrval  22022  mpfrcl  22193  evlsval  22194  mamufval  22506  mat1dimscm  22589  mdetunilem3  22728  mdetunilem4  22729  mdetunilem9  22734  txindislem  23747  txtube  23754  txcmplem1  23755  txhaus  23761  xkoinjcn  23801  pt1hmeo  23920  tsmsxplem1  24267  tsmsxplem2  24268  cnmpopc  25044  dchrval  27352  axlowdimlem15  29211  axlowdim  29216  0ofval  31044  fconst7v  32873  hashxpe  33060  erlval  33486  fracbas  33536  esumcvg  34388  sxbrsigalem0  34573  sxbrsigalem3  34574  sxbrsigalem2  34588  ofcccat  34845  lpadval  34978  lpadlem3  34980  mexval2  35861  csbfinxpg  37889  poimirlem1  38127  poimirlem2  38128  poimirlem3  38129  poimirlem4  38130  poimirlem5  38131  poimirlem6  38132  poimirlem7  38133  poimirlem8  38134  poimirlem10  38136  poimirlem11  38137  poimirlem12  38138  poimirlem15  38141  poimirlem16  38142  poimirlem17  38143  poimirlem18  38144  poimirlem19  38145  poimirlem20  38146  poimirlem21  38147  poimirlem22  38148  poimirlem23  38149  poimirlem24  38150  poimirlem26  38152  poimirlem27  38153  poimirlem28  38154  poimirlem32  38158  sdclem1  38249  ismrer1  38344  ldualset  39756  dibval  41773  dibval3N  41777  dib0  41795  dihwN  41920  hdmap1fval  42427  fsuppssind  43182  mzpclval  43313  mendval  43763  dmrnxp  49467  diag1f1olem  50163  diag2f1olem  50166  prstcval  50181  prstchomval  50189