Theorem xpeq12d 5621

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-opab 5142  df-xp 5596

This theorem is referenced by:  sqxpeqd  5622  opeliunxp  5655  mpomptsx  7897  dmmpossx  7899  fmpox  7900  ovmptss  7924  fparlem3  7945  fparlem4  7946  erssxp  8504  marypha2lem2  9173  ackbij1lem8  9984  r1om  10001  fictb  10002  axcc2lem  10193  axcc2  10194  axdc4lem  10212  fsum2dlem  15480  fsumcom2  15484  ackbijnn  15538  fprod2dlem  15688  fprodcom2  15692  homaval  17744  xpcval  17892  xpchom  17895  xpchom2  17901  1stfval  17906  2ndfval  17909  xpcpropd  17924  evlfval  17933  efmnd  18507  isga  18895  gsumcom2  19574  gsumxp  19575  ablfaclem3  19688  psrval  21116  mamufval  21532  mamudm  21535  mvmulfval  21689  mavmuldm  21697  mavmul0g  21700  txbas  22716  ptbasfi  22730  txindis  22783  tmsxps  23690  metustexhalf  23710  aciunf1lem  30995  gsumpart  31311  fedgmullem1  31706  esum2dlem  32056  lpadval  32652  cvmliftlem15  33256  mexval  33460  mpstval  33493  mclsval  33521  mclsax  33527  mclsppslem  33541  on2recsov  33823  naddcllem  33827  noxpordpred  34106  filnetlem4  34566  poimirlem26  35799  poimirlem28  35801  heiborlem3  35967  elrefrels2  36631  refreleq  36634  elcnvrefrels2  36644  dvhfset  39090  dvhset  39091  dibffval  39150  dibfval  39151  hdmap1fval  39806  opeliun2xp  45637  dmmpossx2  45641  functhinclem1  46291  functhinclem3  46293  functhinclem4  46294