Theorem xpeq12d 5716

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-opab 5206  df-xp 5691

This theorem is referenced by:  sqxpeqd  5717  opeliunxp  5752  opeliun2xp  5753  mpomptsx  8089  dmmpossx  8091  fmpox  8092  ovmptss  8118  fparlem3  8139  fparlem4  8140  on2recsov  8706  naddcllem  8714  erssxp  8768  marypha2lem2  9476  ackbij1lem8  10266  r1om  10283  fictb  10284  axcc2lem  10476  axcc2  10477  axdc4lem  10495  fsum2dlem  15806  fsumcom2  15810  ackbijnn  15864  fprod2dlem  16016  fprodcom2  16020  homaval  18076  xpcval  18222  xpchom  18225  xpchom2  18231  1stfval  18236  2ndfval  18239  xpcpropd  18253  evlfval  18262  efmnd  18883  isga  19309  gsumcom2  19993  gsumxp  19994  ablfaclem3  20107  psrval  21935  mamufval  22396  mamudm  22399  mvmulfval  22548  mavmuldm  22556  mavmul0g  22559  txbas  23575  ptbasfi  23589  txindis  23642  tmsxps  24549  metustexhalf  24569  noxpordpred  27986  aciunf1lem  32672  gsumpart  33060  gsumwrd2dccatlem  33069  gsumwrd2dccat  33070  erlval  33262  rlocval  33263  fedgmullem1  33680  fldextrspunlsplem  33723  esum2dlem  34093  lpadval  34691  cvmliftlem15  35303  mexval  35507  mpstval  35540  mclsval  35568  mclsax  35574  mclsppslem  35588  filnetlem4  36382  poimirlem26  37653  poimirlem28  37655  heiborlem3  37820  cnvref4  38351  elrefrels2  38519  refreleq  38522  elcnvrefrels2  38535  dvhfset  41082  dvhset  41083  dibffval  41142  dibfval  41143  hdmap1fval  41798  dmmpossx2  48253  swapf2f1oaALT  48984  fucofvalg  49013  fucofvalne  49020  fucof21  49042  functhinclem1  49093  functhinclem3  49095  functhinclem4  49096