Theorem xpeq1d 5679

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   × cxp 5648

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-opab 5167  df-xp 5656

This theorem is used by:  csbres  5972  xpssres  6006  curry1  8118  fparlem3  8128  fparlem4  8129  xpord2pred  8165  xpord3pred  8172  naddcllem  8689  ixpsnf1o  8970  dfac5lem3  10208  dfac5lem4  10209  hashxplem  14582  repsw1  14939  subgga  19520  gasubg  19522  sylow2blem2  19841  psrval  22229  mpfrcl  22400  evlsval  22401  mamufval  22713  mat1dimscm  22796  mdetunilem3  22935  mdetunilem4  22936  mdetunilem9  22941  txindislem  23958  txtube  23965  txcmplem1  23966  txhaus  23972  xkoinjcn  24012  pt1hmeo  24131  tsmsxplem1  24478  tsmsxplem2  24479  cnmpopc  25255  dchrval  27567  axlowdimlem15  29540  axlowdim  29545  0ofval  31395  fconst7v  33262  hashxpe  33446  erlval  33866  fracbas  33914  esumcvg  34765  sxbrsigalem0  34950  sxbrsigalem3  34951  sxbrsigalem2  34965  ofcccat  35222  lpadval  35355  lpadlem3  35357  mexval2  36355  csbfinxpg  38405  poimirlem1  38633  poimirlem2  38634  poimirlem3  38635  poimirlem4  38636  poimirlem5  38637  poimirlem6  38638  poimirlem7  38639  poimirlem8  38640  poimirlem10  38642  poimirlem11  38643  poimirlem12  38644  poimirlem15  38647  poimirlem16  38648  poimirlem17  38649  poimirlem18  38650  poimirlem19  38651  poimirlem20  38652  poimirlem21  38653  poimirlem22  38654  poimirlem23  38655  poimirlem24  38656  poimirlem26  38658  poimirlem27  38659  poimirlem28  38660  poimirlem32  38664  sdclem1  38771  ismrer1  38866  ldualset  40276  dibval  42293  dibval3N  42297  dib0  42315  dihwN  42440  hdmap1fval  42947  fsuppssind  43715  mzpclval  43830  mendval  44275  dmrnxp  50042  diag1f1olem  50762  diag2f1olem  50768  prstcval  50783  prstchomval  50791