Theorem xpeq12d 5588

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

Syntax hints:   → wi 4   = wceq 1537   × cxp 5555

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-opab 5131  df-xp 5563

This theorem is referenced by:  sqxpeqd  5589  opeliunxp  5621  mpomptsx  7764  dmmpossx  7766  fmpox  7767  ovmptss  7790  fparlem3  7811  fparlem4  7812  erssxp  8314  marypha2lem2  8902  ackbij1lem8  9651  r1om  9668  fictb  9669  axcc2lem  9860  axcc2  9861  axdc4lem  9879  fsum2dlem  15127  fsumcom2  15131  ackbijnn  15185  fprod2dlem  15336  fprodcom2  15340  homaval  17293  xpcval  17429  xpchom  17432  xpchom2  17438  1stfval  17443  2ndfval  17446  xpcpropd  17460  evlfval  17469  efmnd  18037  isga  18423  gsumcom2  19097  gsumxp  19098  ablfaclem3  19211  psrval  20144  mamufval  20998  mamudm  21001  mvmulfval  21153  mavmuldm  21161  mavmul0g  21164  txbas  22177  ptbasfi  22191  txindis  22244  tmsxps  23148  metustexhalf  23168  aciunf1lem  30409  fedgmullem1  31027  esum2dlem  31353  lpadval  31949  cvmliftlem15  32547  mexval  32751  mpstval  32784  mclsval  32812  mclsax  32818  mclsppslem  32832  filnetlem4  33731  poimirlem26  34920  poimirlem28  34922  heiborlem3  35093  elrefrels2  35759  refreleq  35762  elcnvrefrels2  35772  dvhfset  38218  dvhset  38219  dibffval  38278  dibfval  38279  hdmap1fval  38934  opeliun2xp  44388  dmmpossx2  44392