Theorem xpeq1d 5645

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

Syntax hints:   → wi 4   = wceq 1541   × cxp 5614

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-opab 5154  df-xp 5622

This theorem is referenced by:  csbres  5931  xpssres  5967  curry1  8034  fparlem3  8044  fparlem4  8045  xpord2pred  8075  xpord3pred  8082  naddcllem  8591  ixpsnf1o  8862  dfac5lem3  10016  dfac5lem4  10017  dfac5lem4OLD  10019  hashxplem  14340  repsw1  14690  subgga  19213  gasubg  19215  sylow2blem2  19534  psrval  21853  mpfrcl  22021  evlsval  22022  mamufval  22308  mat1dimscm  22391  mdetunilem3  22530  mdetunilem4  22531  mdetunilem9  22536  txindislem  23549  txtube  23556  txcmplem1  23557  txhaus  23563  xkoinjcn  23603  pt1hmeo  23722  tsmsxplem1  24069  tsmsxplem2  24070  cnmpopc  24850  dchrval  27173  axlowdimlem15  28935  axlowdim  28940  0ofval  30765  fconst7v  32601  hashxpe  32787  erlval  33223  fracbas  33269  esumcvg  34097  sxbrsigalem0  34282  sxbrsigalem3  34283  sxbrsigalem2  34297  ofcccat  34554  lpadval  34687  lpadlem3  34689  mexval2  35545  csbfinxpg  37428  poimirlem1  37667  poimirlem2  37668  poimirlem3  37669  poimirlem4  37670  poimirlem5  37671  poimirlem6  37672  poimirlem7  37673  poimirlem8  37674  poimirlem10  37676  poimirlem11  37677  poimirlem12  37678  poimirlem15  37681  poimirlem16  37682  poimirlem17  37683  poimirlem18  37684  poimirlem19  37685  poimirlem20  37686  poimirlem21  37687  poimirlem22  37688  poimirlem23  37689  poimirlem24  37690  poimirlem26  37692  poimirlem27  37693  poimirlem28  37694  poimirlem32  37698  sdclem1  37789  ismrer1  37884  ldualset  39170  dibval  41187  dibval3N  41191  dib0  41209  dihwN  41334  hdmap1fval  41841  fsuppssind  42632  mzpclval  42764  mendval  43218  dmrnxp  48874  diag1f1olem  49571  diag2f1olem  49574  prstcval  49589  prstchomval  49597