Theorem xpeq12d 5654

Description: Equality deduction for Cartesian product. (Contributed by NM, 8-Dec-2013.)

Hypotheses

Ref	Expression
xpeq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)
xpeq12d.2	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

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

Proof of Theorem xpeq12d

Step	Hyp	Ref	Expression
1		xpeq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		xpeq12d.2	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
3		xpeq12 5648	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 × 𝐶) = (𝐵 × 𝐷))
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → (𝐴 × 𝐶) = (𝐵 × 𝐷))

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-opab 5158  df-xp 5629

This theorem is referenced by:  sqxpeqd  5655  opeliunxp  5690  opeliun2xp  5691  mpomptsx  8006  dmmpossx  8008  fmpox  8009  ovmptss  8033  fparlem3  8054  fparlem4  8055  on2recsov  8593  naddcllem  8601  erssxp  8655  marypha2lem2  9345  ackbij1lem8  10139  r1om  10156  fictb  10157  axcc2lem  10349  axcc2  10350  axdc4lem  10368  fsum2dlem  15695  fsumcom2  15699  ackbijnn  15753  fprod2dlem  15905  fprodcom2  15909  homaval  17956  xpcval  18101  xpchom  18104  xpchom2  18110  1stfval  18115  2ndfval  18118  xpcpropd  18132  evlfval  18141  efmnd  18762  isga  19188  gsumcom2  19872  gsumxp  19873  ablfaclem3  19986  psrval  21840  mamufval  22295  mamudm  22298  mvmulfval  22445  mavmuldm  22453  mavmul0g  22456  txbas  23470  ptbasfi  23484  txindis  23537  tmsxps  24440  metustexhalf  24460  noxpordpred  27883  aciunf1lem  32619  gsumpart  33023  gsumwrd2dccatlem  33032  gsumwrd2dccat  33033  erlval  33208  rlocval  33209  fedgmullem1  33601  fldextrspunlsplem  33644  esum2dlem  34058  lpadval  34643  cvmliftlem15  35270  mexval  35474  mpstval  35507  mclsval  35535  mclsax  35541  mclsppslem  35555  filnetlem4  36354  poimirlem26  37625  poimirlem28  37627  heiborlem3  37792  cnvref4  38317  elrefrels2  38494  refreleq  38497  elcnvrefrels2  38510  dvhfset  41059  dvhset  41060  dibffval  41119  dibfval  41120  hdmap1fval  41775  dmmpossx2  48322  dmrnxp  48822  imasubclem3  49092  imaf1hom  49094  swapf2f1oaALT  49264  fucofvalg  49304  fucofvalne  49311  fucof21  49333  functhinclem1  49430  functhinclem3  49432  functhinclem4  49433