Theorem xpeq12d 5655

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

Syntax hints:   → wi 4   = wceq 1541   × cxp 5622

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-opab 5161  df-xp 5630

This theorem is referenced by:  sqxpeqd  5656  opeliunxp  5691  opeliun2xp  5692  mpomptsx  8008  dmmpossx  8010  fmpox  8011  ovmptss  8035  fparlem3  8056  fparlem4  8057  on2recsov  8596  naddcllem  8604  erssxp  8658  marypha2lem2  9339  ackbij1lem8  10136  r1om  10153  fictb  10154  axcc2lem  10346  axcc2  10347  axdc4lem  10365  fsum2dlem  15693  fsumcom2  15697  ackbijnn  15751  fprod2dlem  15903  fprodcom2  15907  homaval  17955  xpcval  18100  xpchom  18103  xpchom2  18109  1stfval  18114  2ndfval  18117  xpcpropd  18131  evlfval  18140  efmnd  18795  isga  19220  gsumcom2  19904  gsumxp  19905  ablfaclem3  20018  psrval  21871  mamufval  22336  mamudm  22339  mvmulfval  22486  mavmuldm  22494  mavmul0g  22497  txbas  23511  ptbasfi  23525  txindis  23578  tmsxps  24480  metustexhalf  24500  noxpordpred  27949  aciunf1lem  32740  gsumpart  33146  gsumwrd2dccatlem  33159  gsumwrd2dccat  33160  erlval  33340  rlocval  33341  fedgmullem1  33786  fldextrspunlsplem  33830  esum2dlem  34249  lpadval  34833  cvmliftlem15  35492  mexval  35696  mpstval  35729  mclsval  35757  mclsax  35763  mclsppslem  35777  filnetlem4  36575  poimirlem26  37843  poimirlem28  37845  heiborlem3  38010  cnvref4  38539  elrefrels2  38767  refreleq  38770  elcnvrefrels2  38783  dvhfset  41336  dvhset  41337  dibffval  41396  dibfval  41397  hdmap1fval  42052  dmmpossx2  48579  dmrnxp  49078  imasubclem3  49347  imaf1hom  49349  swapf2f1oaALT  49519  fucofvalg  49559  fucofvalne  49566  fucof21  49588  functhinclem1  49685  functhinclem3  49687  functhinclem4  49688