Theorem xpeq2d 5651

Description: Equality deduction for Cartesian product. (Contributed by Jeff Madsen, 17-Jun-2010.)

Hypothesis

Ref	Expression
xpeq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
xpeq2d	⊢ (𝜑 → (𝐶 × 𝐴) = (𝐶 × 𝐵))

Proof of Theorem xpeq2d

Step	Hyp	Ref	Expression
1		xpeq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		xpeq2 5642	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 × 𝐴) = (𝐶 × 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐶 × 𝐴) = (𝐶 × 𝐵))

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

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 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-opab 5158  df-xp 5627

This theorem is referenced by:  xpriindi  5782  csbres  5938  fconstg  6718  curry2  8046  fparlem4  8054  xpord2pred  8084  xpord3pred  8091  naddcllem  8600  fvdiagfn  8825  mapsncnv  8827  xpsneng  8986  axdc4lem  10357  fpwwe2lem12  10544  expval  13977  imasvscafn  17449  fuchom  17879  homafval  17944  setcmon  18002  pwsco2mhm  18749  frmdplusg  18770  smndex1igid  18820  mulgfval  18990  mulgfvalALT  18991  mulgval  18992  efgval  19637  rngqipbas  21241  pzriprnglem13  21439  pzriprnglem14  21440  pjfval  21652  frlmval  21694  islindf5  21785  psrplusg  21883  psrvscafval  21895  psrvsca  21896  opsrle  21993  evlsvvval  22039  evlssca  22040  mpfind  22061  coe1fv  22138  coe1tm  22206  pf1ind  22290  mdetunilem4  22550  mdetunilem9  22555  txindislem  23568  txcmplem2  23577  txhaus  23582  txkgen  23587  xkofvcn  23619  xkoinjcn  23622  cnextval  23996  cnextfval  23997  pcorev2  24975  pcophtb  24976  pi1grplem  24996  pi1inv  24999  dvfval  25845  dvnfval  25871  0dgrb  26198  dgrnznn  26199  dgreq0  26218  dgrmulc  26224  plyrem  26260  facth  26261  fta1  26263  aaliou2  26295  taylfval  26313  taylpfval  26319  expsval  28368  0ofval  30788  2ndresdju  32653  aciunf1  32667  hashxpe  32815  indval2  32861  gsumpart  33074  esplyfval2  33651  vieta  33664  ply1degltdimlem  33707  extdgfialglem1  33777  sxbrsigalem3  34357  sxbrsigalem2  34371  eulerpartlemgu  34462  sseqval  34473  sconnpht  35345  sconnpht2  35354  sconnpi1  35355  cvmlift2lem11  35429  cvmlift2lem12  35430  cvmlift2lem13  35431  cvmlift3lem9  35443  sat1el2xp  35495  mexval  35618  mexval2  35619  mdvval  35620  mpstval  35651  elima4  35892  bj-xtageq  37105  matunitlindflem1  37729  poimirlem32  37765  ismrer1  37951  ecxrncnvep2  38507  lflsc0N  39255  lkrscss  39270  lfl1dim  39293  lfl1dim2N  39294  ldualvs  39309  evlsevl  42732  0prjspnrel  42785  mzpclval  42882  mzpcl1  42886  mendvsca  43344  dvconstbi  44491  expgrowth  44492  gpgov  48204  dmrnxp  48998  fucofvalne  49486