Theorem xpeq1d 5665

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

Syntax hints:   → wi 4   = wceq 1550   × cxp 5634

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-opab 5153  df-xp 5642

This theorem is referenced by:  csbres  5957  xpssres  5993  curry1  8067  fparlem3  8077  fparlem4  8078  xpord2pred  8109  xpord3pred  8116  naddcllem  8630  ixpsnf1o  8905  dfac5lem3  10067  dfac5lem4  10068  dfac5lem4OLD  10070  hashxplem  14432  repsw1  14782  subgga  19312  gasubg  19314  sylow2blem2  19633  psrval  21936  mpfrcl  22107  evlsval  22108  mamufval  22421  mat1dimscm  22504  mdetunilem3  22643  mdetunilem4  22644  mdetunilem9  22649  txindislem  23662  txtube  23669  txcmplem1  23670  txhaus  23676  xkoinjcn  23716  pt1hmeo  23835  tsmsxplem1  24182  tsmsxplem2  24183  cnmpopc  24959  dchrval  27264  axlowdimlem15  29092  axlowdim  29097  0ofval  30925  fconst7v  32761  hashxpe  32948  erlval  33388  fracbas  33438  esumcvg  34327  sxbrsigalem0  34512  sxbrsigalem3  34513  sxbrsigalem2  34527  ofcccat  34784  lpadval  34920  lpadlem3  34922  mexval2  35791  csbfinxpg  37820  poimirlem1  38058  poimirlem2  38059  poimirlem3  38060  poimirlem4  38061  poimirlem5  38062  poimirlem6  38063  poimirlem7  38064  poimirlem8  38065  poimirlem10  38067  poimirlem11  38068  poimirlem12  38069  poimirlem15  38072  poimirlem16  38073  poimirlem17  38074  poimirlem18  38075  poimirlem19  38076  poimirlem20  38077  poimirlem21  38078  poimirlem22  38079  poimirlem23  38080  poimirlem24  38081  poimirlem26  38083  poimirlem27  38084  poimirlem28  38085  poimirlem32  38089  sdclem1  38180  ismrer1  38275  ldualset  39687  dibval  41704  dibval3N  41708  dib0  41726  dihwN  41851  hdmap1fval  42358  fsuppssind  43113  mzpclval  43244  mendval  43694  dmrnxp  49396  diag1f1olem  50092  diag2f1olem  50095  prstcval  50110  prstchomval  50118