Theorem xpeq12d 5708

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-opab 5212  df-xp 5683

This theorem is referenced by:  sqxpeqd  5709  opeliunxp  5744  mpomptsx  8050  dmmpossx  8052  fmpox  8053  ovmptss  8079  fparlem3  8100  fparlem4  8101  on2recsov  8667  naddcllem  8675  erssxp  8726  marypha2lem2  9431  ackbij1lem8  10222  r1om  10239  fictb  10240  axcc2lem  10431  axcc2  10432  axdc4lem  10450  fsum2dlem  15716  fsumcom2  15720  ackbijnn  15774  fprod2dlem  15924  fprodcom2  15928  homaval  17981  xpcval  18129  xpchom  18132  xpchom2  18138  1stfval  18143  2ndfval  18146  xpcpropd  18161  evlfval  18170  efmnd  18751  isga  19155  gsumcom2  19843  gsumxp  19844  ablfaclem3  19957  psrval  21468  mamufval  21887  mamudm  21890  mvmulfval  22044  mavmuldm  22052  mavmul0g  22055  txbas  23071  ptbasfi  23085  txindis  23138  tmsxps  24045  metustexhalf  24065  noxpordpred  27437  aciunf1lem  31887  gsumpart  32207  fedgmullem1  32714  esum2dlem  33090  lpadval  33688  cvmliftlem15  34289  mexval  34493  mpstval  34526  mclsval  34554  mclsax  34560  mclsppslem  34574  filnetlem4  35266  poimirlem26  36514  poimirlem28  36516  heiborlem3  36681  cnvref4  37219  elrefrels2  37388  refreleq  37391  elcnvrefrels2  37404  dvhfset  39951  dvhset  39952  dibffval  40011  dibfval  40012  hdmap1fval  40667  opeliun2xp  47008  dmmpossx2  47012  functhinclem1  47661  functhinclem3  47663  functhinclem4  47664