Theorem xpeq12d 5662

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

Syntax hints:   → wi 4   = wceq 1542   × cxp 5629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-opab 5148  df-xp 5637

This theorem is referenced by:  sqxpeqd  5663  opeliunxp  5698  opeliun2xp  5699  mpomptsx  8017  dmmpossx  8019  fmpox  8020  ovmptss  8043  fparlem3  8064  fparlem4  8065  on2recsov  8604  naddcllem  8612  erssxp  8667  marypha2lem2  9349  ackbij1lem8  10148  r1om  10165  fictb  10166  axcc2lem  10358  axcc2  10359  axdc4lem  10377  fsum2dlem  15732  fsumcom2  15736  ackbijnn  15793  fprod2dlem  15945  fprodcom2  15949  homaval  17998  xpcval  18143  xpchom  18146  xpchom2  18152  1stfval  18157  2ndfval  18160  xpcpropd  18174  evlfval  18183  efmnd  18838  isga  19266  gsumcom2  19950  gsumxp  19951  ablfaclem3  20064  psrval  21895  mamufval  22357  mamudm  22360  mvmulfval  22507  mavmuldm  22515  mavmul0g  22518  txbas  23532  ptbasfi  23546  txindis  23599  tmsxps  24501  metustexhalf  24521  noxpordpred  27945  aciunf1lem  32735  gsumpart  33124  gsumwrd2dccatlem  33138  gsumwrd2dccat  33139  erlval  33319  rlocval  33320  fedgmullem1  33773  fldextrspunlsplem  33817  esum2dlem  34236  lpadval  34820  cvmliftlem15  35480  mexval  35684  mpstval  35717  mclsval  35745  mclsax  35751  mclsppslem  35765  filnetlem4  36563  poimirlem26  37967  poimirlem28  37969  heiborlem3  38134  cnvref4  38671  elrefrels2  38919  refreleq  38922  elcnvrefrels2  38935  dvhfset  41526  dvhset  41527  dibffval  41586  dibfval  41587  hdmap1fval  42242  dmmpossx2  48813  dmrnxp  49312  imasubclem3  49581  imaf1hom  49583  swapf2f1oaALT  49753  fucofvalg  49793  fucofvalne  49800  fucof21  49822  functhinclem1  49919  functhinclem3  49921  functhinclem4  49922