Theorem xpeq12d 5663

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-opab 5163  df-xp 5638

This theorem is referenced by:  sqxpeqd  5664  opeliunxp  5699  opeliun2xp  5700  mpomptsx  8018  dmmpossx  8020  fmpox  8021  ovmptss  8045  fparlem3  8066  fparlem4  8067  on2recsov  8606  naddcllem  8614  erssxp  8669  marypha2lem2  9351  ackbij1lem8  10148  r1om  10165  fictb  10166  axcc2lem  10358  axcc2  10359  axdc4lem  10377  fsum2dlem  15705  fsumcom2  15709  ackbijnn  15763  fprod2dlem  15915  fprodcom2  15919  homaval  17967  xpcval  18112  xpchom  18115  xpchom2  18121  1stfval  18126  2ndfval  18129  xpcpropd  18143  evlfval  18152  efmnd  18807  isga  19232  gsumcom2  19916  gsumxp  19917  ablfaclem3  20030  psrval  21883  mamufval  22348  mamudm  22351  mvmulfval  22498  mavmuldm  22506  mavmul0g  22509  txbas  23523  ptbasfi  23537  txindis  23590  tmsxps  24492  metustexhalf  24512  noxpordpred  27961  aciunf1lem  32751  gsumpart  33156  gsumwrd2dccatlem  33170  gsumwrd2dccat  33171  erlval  33351  rlocval  33352  fedgmullem1  33806  fldextrspunlsplem  33850  esum2dlem  34269  lpadval  34853  cvmliftlem15  35511  mexval  35715  mpstval  35748  mclsval  35776  mclsax  35782  mclsppslem  35796  filnetlem4  36594  poimirlem26  37891  poimirlem28  37893  heiborlem3  38058  cnvref4  38595  elrefrels2  38843  refreleq  38846  elcnvrefrels2  38859  dvhfset  41450  dvhset  41451  dibffval  41510  dibfval  41511  hdmap1fval  42166  dmmpossx2  48691  dmrnxp  49190  imasubclem3  49459  imaf1hom  49461  swapf2f1oaALT  49631  fucofvalg  49671  fucofvalne  49678  fucof21  49700  functhinclem1  49797  functhinclem3  49799  functhinclem4  49800