Theorem xpeq12d 5631

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

Syntax hints:   → wi 4   = wceq 1539   × cxp 5598

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-opab 5144  df-xp 5606

This theorem is referenced by:  sqxpeqd  5632  opeliunxp  5665  mpomptsx  7936  dmmpossx  7938  fmpox  7939  ovmptss  7965  fparlem3  7986  fparlem4  7987  erssxp  8552  marypha2lem2  9243  ackbij1lem8  10033  r1om  10050  fictb  10051  axcc2lem  10242  axcc2  10243  axdc4lem  10261  fsum2dlem  15531  fsumcom2  15535  ackbijnn  15589  fprod2dlem  15739  fprodcom2  15743  homaval  17795  xpcval  17943  xpchom  17946  xpchom2  17952  1stfval  17957  2ndfval  17960  xpcpropd  17975  evlfval  17984  efmnd  18558  isga  18946  gsumcom2  19625  gsumxp  19626  ablfaclem3  19739  psrval  21167  mamufval  21583  mamudm  21586  mvmulfval  21740  mavmuldm  21748  mavmul0g  21751  txbas  22767  ptbasfi  22781  txindis  22834  tmsxps  23741  metustexhalf  23761  aciunf1lem  31048  gsumpart  31364  fedgmullem1  31759  esum2dlem  32109  lpadval  32705  cvmliftlem15  33309  mexval  33513  mpstval  33546  mclsval  33574  mclsax  33580  mclsppslem  33594  on2recsov  33876  naddcllem  33880  noxpordpred  34159  filnetlem4  34619  poimirlem26  35851  poimirlem28  35853  heiborlem3  36019  cnvref4  36563  elrefrels2  36732  refreleq  36735  elcnvrefrels2  36748  dvhfset  39294  dvhset  39295  dibffval  39354  dibfval  39355  hdmap1fval  40010  opeliun2xp  45912  dmmpossx2  45916  functhinclem1  46566  functhinclem3  46568  functhinclem4  46569