Theorem xpeq1d 5586

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

Syntax hints:   → wi 4   = wceq 1537   × cxp 5555

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-opab 5131  df-xp 5563

This theorem is referenced by:  csbres  5858  xpssres  5891  curry1  7801  fparlem3  7811  fparlem4  7812  ixpsnf1o  8504  xpfi  8791  dfac5lem3  9553  dfac5lem4  9554  hashxplem  13797  repsw1  14147  subgga  18432  gasubg  18434  sylow2blem2  18748  psrval  20144  mpfrcl  20300  evlsval  20301  mamufval  20998  mat1dimscm  21086  mdetunilem3  21225  mdetunilem4  21226  mdetunilem9  21231  txindislem  22243  txtube  22250  txcmplem1  22251  txhaus  22257  xkoinjcn  22297  pt1hmeo  22416  tsmsxplem1  22763  tsmsxplem2  22764  cnmpopc  23534  dchrval  25812  axlowdimlem15  26744  axlowdim  26749  0ofval  28566  hashxpe  30531  esumcvg  31347  sxbrsigalem0  31531  sxbrsigalem3  31532  sxbrsigalem2  31546  ofcccat  31815  lpadval  31949  lpadlem3  31951  mexval2  32752  csbfinxpg  34671  poimirlem1  34895  poimirlem2  34896  poimirlem3  34897  poimirlem4  34898  poimirlem5  34899  poimirlem6  34900  poimirlem7  34901  poimirlem8  34902  poimirlem10  34904  poimirlem11  34905  poimirlem12  34906  poimirlem15  34909  poimirlem16  34910  poimirlem17  34911  poimirlem18  34912  poimirlem19  34913  poimirlem20  34914  poimirlem21  34915  poimirlem22  34916  poimirlem23  34917  poimirlem24  34918  poimirlem26  34920  poimirlem27  34921  poimirlem28  34922  poimirlem32  34926  sdclem1  35020  ismrer1  35118  ldualset  36263  dibval  38280  dibval3N  38284  dib0  38302  dihwN  38427  hdmap1fval  38934  mzpclval  39329  mendval  39790