Theorem xpeq12d 5719

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

Syntax hints:   → wi 4   = wceq 1536   × cxp 5686

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-opab 5210  df-xp 5694

This theorem is referenced by:  sqxpeqd  5720  opeliunxp  5755  mpomptsx  8087  dmmpossx  8089  fmpox  8090  ovmptss  8116  fparlem3  8137  fparlem4  8138  on2recsov  8704  naddcllem  8712  erssxp  8766  marypha2lem2  9473  ackbij1lem8  10263  r1om  10280  fictb  10281  axcc2lem  10473  axcc2  10474  axdc4lem  10492  fsum2dlem  15802  fsumcom2  15806  ackbijnn  15860  fprod2dlem  16012  fprodcom2  16016  homaval  18084  xpcval  18232  xpchom  18235  xpchom2  18241  1stfval  18246  2ndfval  18249  xpcpropd  18264  evlfval  18273  efmnd  18895  isga  19321  gsumcom2  20007  gsumxp  20008  ablfaclem3  20121  psrval  21952  mamufval  22411  mamudm  22414  mvmulfval  22563  mavmuldm  22571  mavmul0g  22574  txbas  23590  ptbasfi  23604  txindis  23657  tmsxps  24564  metustexhalf  24584  noxpordpred  28000  aciunf1lem  32678  gsumpart  33042  gsumwrd2dccatlem  33051  gsumwrd2dccat  33052  erlval  33244  rlocval  33245  fedgmullem1  33656  esum2dlem  34072  lpadval  34669  cvmliftlem15  35282  mexval  35486  mpstval  35519  mclsval  35547  mclsax  35553  mclsppslem  35567  filnetlem4  36363  poimirlem26  37632  poimirlem28  37634  heiborlem3  37799  cnvref4  38331  elrefrels2  38499  refreleq  38502  elcnvrefrels2  38515  dvhfset  41062  dvhset  41063  dibffval  41122  dibfval  41123  hdmap1fval  41778  opeliun2xp  48177  dmmpossx2  48181  functhinclem1  48840  functhinclem3  48842  functhinclem4  48843