Theorem xpeq1d 5587

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

Syntax hints:   → wi 4   = wceq 1536   × cxp 5556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-opab 5132  df-xp 5564

This theorem is referenced by:  csbres  5859  xpssres  5892  curry1  7802  fparlem3  7812  fparlem4  7813  ixpsnf1o  8505  xpfi  8792  dfac5lem3  9554  dfac5lem4  9555  hashxplem  13797  repsw1  14148  subgga  18433  gasubg  18435  sylow2blem2  18749  psrval  20145  mpfrcl  20301  evlsval  20302  mamufval  20999  mat1dimscm  21087  mdetunilem3  21226  mdetunilem4  21227  mdetunilem9  21232  txindislem  22244  txtube  22251  txcmplem1  22252  txhaus  22258  xkoinjcn  22298  pt1hmeo  22417  tsmsxplem1  22764  tsmsxplem2  22765  cnmpopc  23535  dchrval  25813  axlowdimlem15  26745  axlowdim  26750  0ofval  28567  hashxpe  30532  esumcvg  31349  sxbrsigalem0  31533  sxbrsigalem3  31534  sxbrsigalem2  31548  ofcccat  31817  lpadval  31951  lpadlem3  31953  mexval2  32754  csbfinxpg  34673  poimirlem1  34897  poimirlem2  34898  poimirlem3  34899  poimirlem4  34900  poimirlem5  34901  poimirlem6  34902  poimirlem7  34903  poimirlem8  34904  poimirlem10  34906  poimirlem11  34907  poimirlem12  34908  poimirlem15  34911  poimirlem16  34912  poimirlem17  34913  poimirlem18  34914  poimirlem19  34915  poimirlem20  34916  poimirlem21  34917  poimirlem22  34918  poimirlem23  34919  poimirlem24  34920  poimirlem26  34922  poimirlem27  34923  poimirlem28  34924  poimirlem32  34928  sdclem1  35022  ismrer1  35120  ldualset  36265  dibval  38282  dibval3N  38286  dib0  38304  dihwN  38429  hdmap1fval  38936  mzpclval  39328  mendval  39789