Theorem xpeq12d 5676

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 5670	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 × 𝐶) = (𝐵 × 𝐷))
4	1, 2, 3	syl2anc 593	1 ⊢ (𝜑 → (𝐴 × 𝐶) = (𝐵 × 𝐷))

Syntax hints:   → wi 4   = wceq 1559   × cxp 5643

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-opab 5162  df-xp 5651

This theorem is referenced by:  sqxpeqd  5677  opeliunxp  5712  opeliun2xp  5713  mpomptsx  8041  dmmpossx  8043  fmpox  8044  ovmptss  8067  fparlem3  8088  fparlem4  8089  on2recsov  8633  naddcllem  8641  erssxp  8697  marypha2lem2  9379  ackbij1lem8  10179  r1om  10196  fictb  10197  axcc2lem  10390  axcc2  10391  axdc4lem  10409  fsum2dlem  15780  fsumcom2  15784  ackbijnn  15841  fprod2dlem  15993  fprodcom2  15997  homaval  18047  xpcval  18192  xpchom  18195  xpchom2  18201  1stfval  18206  2ndfval  18209  xpcpropd  18223  evlfval  18232  efmnd  18887  isga  19314  gsumcom2  19998  gsumxp  19999  ablfaclem3  20112  psrval  21947  mamufval  22432  mamudm  22435  mvmulfval  22582  mavmuldm  22590  mavmul0g  22593  txbas  23607  ptbasfi  23621  txindis  23674  tmsxps  24576  metustexhalf  24596  noxpordpred  28023  aciunf1lem  32814  gsumpart  33204  gsumwrd2dccatlem  33218  gsumwrd2dccat  33219  erlval  33400  rlocval  33401  fedgmullem1  33887  fldextrspunlsplem  33931  esum2dlem  34350  lpadval  34937  cvmliftlem15  35612  mexval  35816  mpstval  35849  mclsval  35877  mclsax  35883  mclsppslem  35897  filnetlem4  36705  poimirlem26  38109  poimirlem28  38111  heiborlem3  38276  cnvref4  38813  elrefrels2  39061  refreleq  39064  elcnvrefrels2  39077  dvhfset  41668  dvhset  41669  dibffval  41728  dibfval  41729  hdmap1fval  42384  dmmpossx2  48923  dmrnxp  49422  imasubclem3  49691  imaf1hom  49693  swapf2f1oaALT  49863  fucofvalg  49903  fucofvalne  49910  fucof21  49932  functhinclem1  50029  functhinclem3  50031  functhinclem4  50032