Theorem xpeq1d 5172

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

Syntax hints:   → wi 4   = wceq 1523   × cxp 5141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-opab 4746  df-xp 5149

This theorem is referenced by:  csbres  5431  xpssres  5469  curry1  7314  fparlem3  7324  fparlem4  7325  ixpsnf1o  7990  xpfi  8272  dfac5lem3  8986  dfac5lem4  8987  cdaassen  9042  hashxplem  13258  repsw1  13576  subgga  17779  gasubg  17781  sylow2blem2  18082  psrval  19410  mpfrcl  19566  evlsval  19567  mamufval  20239  mat1dimscm  20329  mdetunilem3  20468  mdetunilem4  20469  mdetunilem9  20474  txindislem  21484  txtube  21491  txcmplem1  21492  txhaus  21498  xkoinjcn  21538  pt1hmeo  21657  tsmsxplem1  22003  tsmsxplem2  22004  cnmpt2pc  22774  dchrval  25004  axlowdimlem15  25881  axlowdim  25886  0ofval  27770  esumcvg  30276  sxbrsigalem0  30461  sxbrsigalem3  30462  sxbrsigalem2  30476  ofcccat  30748  mexval2  31526  csbfinxpg  33355  poimirlem1  33540  poimirlem2  33541  poimirlem3  33542  poimirlem4  33543  poimirlem5  33544  poimirlem6  33545  poimirlem7  33546  poimirlem8  33547  poimirlem10  33549  poimirlem11  33550  poimirlem12  33551  poimirlem15  33554  poimirlem16  33555  poimirlem17  33556  poimirlem18  33557  poimirlem19  33558  poimirlem20  33559  poimirlem21  33560  poimirlem22  33561  poimirlem23  33562  poimirlem24  33563  poimirlem26  33565  poimirlem27  33566  poimirlem28  33567  poimirlem32  33571  sdclem1  33669  ismrer1  33767  ldualset  34730  dibval  36748  dibval3N  36752  dib0  36770  dihwN  36895  hdmap1fval  37403  mzpclval  37605  mendval  38070