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  37847  poimirlem28  37849  heiborlem3  38014  cnvref4  38543  elrefrels2  38771  refreleq  38774  elcnvrefrels2  38787  dvhfset  41340  dvhset  41341  dibffval  41400  dibfval  41401  hdmap1fval  42056  dmmpossx2  48583  dmrnxp  49082  imasubclem3  49351  imaf1hom  49353  swapf2f1oaALT  49523  fucofvalg  49563  fucofvalne  49570  fucof21  49592  functhinclem1  49689  functhinclem3  49691  functhinclem4  49692