Theorem xpeq2d 5684

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

Syntax hints:   → wi 4   = wceq 1540   × cxp 5652

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-opab 5182  df-xp 5660

This theorem is referenced by:  xpriindi  5816  csbres  5969  fconstg  6765  curry2  8106  fparlem4  8114  xpord2pred  8144  xpord3pred  8151  naddcllem  8688  fvdiagfn  8905  mapsncnv  8907  xpsneng  9070  axdc4lem  10469  fpwwe2lem12  10656  expval  14081  imasvscafn  17551  fuchom  17977  homafval  18042  setcmon  18100  pwsco2mhm  18811  frmdplusg  18832  smndex1igid  18882  mulgfval  19052  mulgfvalALT  19053  mulgval  19054  efgval  19698  rngqipbas  21256  pzriprnglem13  21454  pzriprnglem14  21455  pjfval  21666  frlmval  21708  islindf5  21799  psrplusg  21896  psrvscafval  21908  psrvsca  21909  opsrle  22005  evlssca  22047  mpfind  22065  coe1fv  22142  coe1tm  22210  pf1ind  22293  mdetunilem4  22553  mdetunilem9  22558  txindislem  23571  txcmplem2  23580  txhaus  23585  txkgen  23590  xkofvcn  23622  xkoinjcn  23625  cnextval  23999  cnextfval  24000  pcorev2  24979  pcophtb  24980  pi1grplem  25000  pi1inv  25003  dvfval  25850  dvnfval  25876  0dgrb  26203  dgrnznn  26204  dgreq0  26223  dgrmulc  26229  plyrem  26265  facth  26266  fta1  26268  aaliou2  26300  taylfval  26318  taylpfval  26324  expsval  28363  0ofval  30768  2ndresdju  32627  aciunf1  32641  hashxpe  32786  indval2  32831  gsumpart  33051  ply1degltdimlem  33662  sxbrsigalem3  34304  sxbrsigalem2  34318  eulerpartlemgu  34409  sseqval  34420  sconnpht  35251  sconnpht2  35260  sconnpi1  35261  cvmlift2lem11  35335  cvmlift2lem12  35336  cvmlift2lem13  35337  cvmlift3lem9  35349  sat1el2xp  35401  mexval  35524  mexval2  35525  mdvval  35526  mpstval  35557  elima4  35793  bj-xtageq  37006  matunitlindflem1  37640  poimirlem32  37676  ismrer1  37862  lflsc0N  39101  lkrscss  39116  lfl1dim  39139  lfl1dim2N  39140  ldualvs  39155  evlsvvval  42586  evlsevl  42594  0prjspnrel  42650  mzpclval  42748  mzpcl1  42752  mendvsca  43211  dvconstbi  44358  expgrowth  44359  gpgov  48046  dmrnxp  48815  fucofvalne  49236