Theorem xpeq12d 5731

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

Syntax hints:   → wi 4   = wceq 1537   × cxp 5698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-opab 5229  df-xp 5706

This theorem is referenced by:  sqxpeqd  5732  opeliunxp  5767  mpomptsx  8105  dmmpossx  8107  fmpox  8108  ovmptss  8134  fparlem3  8155  fparlem4  8156  on2recsov  8724  naddcllem  8732  erssxp  8786  marypha2lem2  9505  ackbij1lem8  10295  r1om  10312  fictb  10313  axcc2lem  10505  axcc2  10506  axdc4lem  10524  fsum2dlem  15818  fsumcom2  15822  ackbijnn  15876  fprod2dlem  16028  fprodcom2  16032  homaval  18098  xpcval  18246  xpchom  18249  xpchom2  18255  1stfval  18260  2ndfval  18263  xpcpropd  18278  evlfval  18287  efmnd  18905  isga  19331  gsumcom2  20017  gsumxp  20018  ablfaclem3  20131  psrval  21958  mamufval  22417  mamudm  22420  mvmulfval  22569  mavmuldm  22577  mavmul0g  22580  txbas  23596  ptbasfi  23610  txindis  23663  tmsxps  24570  metustexhalf  24590  noxpordpred  28004  aciunf1lem  32680  gsumpart  33038  erlval  33230  rlocval  33231  fedgmullem1  33642  esum2dlem  34056  lpadval  34653  cvmliftlem15  35266  mexval  35470  mpstval  35503  mclsval  35531  mclsax  35537  mclsppslem  35551  filnetlem4  36347  poimirlem26  37606  poimirlem28  37608  heiborlem3  37773  cnvref4  38306  elrefrels2  38474  refreleq  38477  elcnvrefrels2  38490  dvhfset  41037  dvhset  41038  dibffval  41097  dibfval  41098  hdmap1fval  41753  opeliun2xp  48057  dmmpossx2  48061  functhinclem1  48708  functhinclem3  48710  functhinclem4  48711