Theorem xpeq12d 5656

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

Syntax hints:   → wi 4   = wceq 1547   × cxp 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-opab 5142  df-xp 5631

This theorem is referenced by:  sqxpeqd  5657  opeliunxp  5692  opeliun2xp  5693  mpomptsx  8013  dmmpossx  8015  fmpox  8016  ovmptss  8039  fparlem3  8060  fparlem4  8061  on2recsov  8601  naddcllem  8609  erssxp  8664  marypha2lem2  9346  ackbij1lem8  10146  r1om  10163  fictb  10164  axcc2lem  10356  axcc2  10357  axdc4lem  10375  fsum2dlem  15730  fsumcom2  15734  ackbijnn  15791  fprod2dlem  15943  fprodcom2  15947  homaval  17996  xpcval  18141  xpchom  18144  xpchom2  18150  1stfval  18155  2ndfval  18158  xpcpropd  18172  evlfval  18181  efmnd  18836  isga  19264  gsumcom2  19948  gsumxp  19949  ablfaclem3  20062  psrval  21897  mamufval  22382  mamudm  22385  mvmulfval  22532  mavmuldm  22540  mavmul0g  22543  txbas  23557  ptbasfi  23571  txindis  23624  tmsxps  24526  metustexhalf  24546  noxpordpred  27970  aciunf1lem  32761  gsumpart  33151  gsumwrd2dccatlem  33165  gsumwrd2dccat  33166  erlval  33346  rlocval  33347  fedgmullem1  33820  fldextrspunlsplem  33864  esum2dlem  34283  lpadval  34867  cvmliftlem15  35533  mexval  35737  mpstval  35770  mclsval  35798  mclsax  35804  mclsppslem  35818  filnetlem4  36616  poimirlem26  38020  poimirlem28  38022  heiborlem3  38187  cnvref4  38724  elrefrels2  38972  refreleq  38975  elcnvrefrels2  38988  dvhfset  41579  dvhset  41580  dibffval  41639  dibfval  41640  hdmap1fval  42295  dmmpossx2  48835  dmrnxp  49334  imasubclem3  49603  imaf1hom  49605  swapf2f1oaALT  49775  fucofvalg  49815  fucofvalne  49822  fucof21  49844  functhinclem1  49941  functhinclem3  49943  functhinclem4  49944