Theorem xpeq2d 5641

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

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

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 5149  df-xp 5617

This theorem is referenced by:  xpriindi  5771  csbres  5926  fconstg  6705  curry2  8032  fparlem4  8040  xpord2pred  8070  xpord3pred  8077  naddcllem  8586  fvdiagfn  8810  mapsncnv  8812  xpsneng  8970  axdc4lem  10341  fpwwe2lem12  10528  expval  13965  imasvscafn  17436  fuchom  17866  homafval  17931  setcmon  17989  pwsco2mhm  18736  frmdplusg  18757  smndex1igid  18807  mulgfval  18977  mulgfvalALT  18978  mulgval  18979  efgval  19624  rngqipbas  21227  pzriprnglem13  21425  pzriprnglem14  21426  pjfval  21638  frlmval  21680  islindf5  21771  psrplusg  21868  psrvscafval  21880  psrvsca  21881  opsrle  21977  evlssca  22019  mpfind  22037  coe1fv  22114  coe1tm  22182  pf1ind  22265  mdetunilem4  22525  mdetunilem9  22530  txindislem  23543  txcmplem2  23552  txhaus  23557  txkgen  23562  xkofvcn  23594  xkoinjcn  23597  cnextval  23971  cnextfval  23972  pcorev2  24950  pcophtb  24951  pi1grplem  24971  pi1inv  24974  dvfval  25820  dvnfval  25846  0dgrb  26173  dgrnznn  26174  dgreq0  26193  dgrmulc  26199  plyrem  26235  facth  26236  fta1  26238  aaliou2  26270  taylfval  26288  taylpfval  26294  expsval  28343  0ofval  30759  2ndresdju  32623  aciunf1  32637  hashxpe  32781  indval2  32827  gsumpart  33029  ply1degltdimlem  33627  extdgfialglem1  33697  sxbrsigalem3  34277  sxbrsigalem2  34291  eulerpartlemgu  34382  sseqval  34393  sconnpht  35265  sconnpht2  35274  sconnpi1  35275  cvmlift2lem11  35349  cvmlift2lem12  35350  cvmlift2lem13  35351  cvmlift3lem9  35363  sat1el2xp  35415  mexval  35538  mexval2  35539  mdvval  35540  mpstval  35571  elima4  35812  bj-xtageq  37022  matunitlindflem1  37656  poimirlem32  37692  ismrer1  37878  lflsc0N  39122  lkrscss  39137  lfl1dim  39160  lfl1dim2N  39161  ldualvs  39176  evlsvvval  42596  evlsevl  42604  0prjspnrel  42660  mzpclval  42758  mzpcl1  42762  mendvsca  43220  dvconstbi  44367  expgrowth  44368  gpgov  48073  dmrnxp  48868  fucofvalne  49357