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  27439  aciunf1lem  31918  gsumpart  32238  fedgmullem1  32745  esum2dlem  33121  lpadval  33719  cvmliftlem15  34320  mexval  34524  mpstval  34557  mclsval  34585  mclsax  34591  mclsppslem  34605  filnetlem4  35314  poimirlem26  36562  poimirlem28  36564  heiborlem3  36729  cnvref4  37267  elrefrels2  37436  refreleq  37439  elcnvrefrels2  37452  dvhfset  39999  dvhset  40000  dibffval  40059  dibfval  40060  hdmap1fval  40715  opeliun2xp  47056  dmmpossx2  47060  functhinclem1  47709  functhinclem3  47711  functhinclem4  47712