Theorem xpeq1d 5685

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   × cxp 5654

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-opab 5172  df-xp 5662

This theorem is used by:  csbres  5985  xpssres  6020  curry1  8145  fparlem3  8155  fparlem4  8156  xpord2pred  8192  xpord3pred  8199  naddcllem  8716  ixpsnf1o  8997  dfac5lem3  10234  dfac5lem4  10235  hashxplem  14608  repsw1  14965  subgga  19547  gasubg  19549  sylow2blem2  19868  psrval  22256  mpfrcl  22427  evlsval  22428  mamufval  22740  mat1dimscm  22823  mdetunilem3  22962  mdetunilem4  22963  mdetunilem9  22968  txindislem  23985  txtube  23992  txcmplem1  23993  txhaus  23999  xkoinjcn  24039  pt1hmeo  24158  tsmsxplem1  24505  tsmsxplem2  24506  cnmpopc  25282  dchrval  27594  axlowdimlem15  29567  axlowdim  29572  0ofval  31422  fconst7v  33289  hashxpe  33472  erlval  33895  fracbas  33951  esumcvg  34801  sxbrsigalem0  34986  sxbrsigalem3  34987  sxbrsigalem2  35001  ofcccat  35258  lpadval  35391  lpadlem3  35393  mexval2  36448  csbfinxpg  38516  poimirlem1  38744  poimirlem2  38745  poimirlem3  38746  poimirlem4  38747  poimirlem5  38748  poimirlem6  38749  poimirlem7  38750  poimirlem8  38751  poimirlem10  38753  poimirlem11  38754  poimirlem12  38755  poimirlem15  38758  poimirlem16  38759  poimirlem17  38760  poimirlem18  38761  poimirlem19  38762  poimirlem20  38763  poimirlem21  38764  poimirlem22  38765  poimirlem23  38766  poimirlem24  38767  poimirlem26  38769  poimirlem27  38770  poimirlem28  38771  poimirlem32  38775  sdclem1  38880  ismrer1  38975  ldualset  40385  dibval  42402  dibval3N  42406  dib0  42424  dihwN  42549  hdmap1fval  43056  fsuppssind  43825  mzpclval  43940  mendval  44384  dmrnxp  50163  diag1f1olem  50883  diag2f1olem  50889  prstcval  50904  prstchomval  50912