Theorem xpeq1d 5306

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

Syntax hints:   → wi 4   = wceq 1652   × cxp 5275

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-opab 4872  df-xp 5283

This theorem is referenced by:  csbres  5568  xpssres  5608  curry1  7471  fparlem3  7481  fparlem4  7482  ixpsnf1o  8153  xpfi  8438  dfac5lem3  9199  dfac5lem4  9200  cdaassen  9257  hashxplem  13421  repsw1  13807  subgga  17996  gasubg  17998  sylow2blem2  18300  psrval  19636  mpfrcl  19791  evlsval  19792  mamufval  20467  mat1dimscm  20558  mdetunilem3  20697  mdetunilem4  20698  mdetunilem9  20703  txindislem  21716  txtube  21723  txcmplem1  21724  txhaus  21730  xkoinjcn  21770  pt1hmeo  21889  tsmsxplem1  22235  tsmsxplem2  22236  cnmpt2pc  23006  dchrval  25250  axlowdimlem15  26127  axlowdim  26132  0ofval  28098  esumcvg  30595  sxbrsigalem0  30780  sxbrsigalem3  30781  sxbrsigalem2  30795  ofcccat  31069  mexval2  31848  csbfinxpg  33658  poimirlem1  33834  poimirlem2  33835  poimirlem3  33836  poimirlem4  33837  poimirlem5  33838  poimirlem6  33839  poimirlem7  33840  poimirlem8  33841  poimirlem10  33843  poimirlem11  33844  poimirlem12  33845  poimirlem15  33848  poimirlem16  33849  poimirlem17  33850  poimirlem18  33851  poimirlem19  33852  poimirlem20  33853  poimirlem21  33854  poimirlem22  33855  poimirlem23  33856  poimirlem24  33857  poimirlem26  33859  poimirlem27  33860  poimirlem28  33861  poimirlem32  33865  sdclem1  33961  ismrer1  34059  ldualset  35081  dibval  37098  dibval3N  37102  dib0  37120  dihwN  37245  hdmap1fval  37752  mzpclval  37966  mendval  38430