Theorem xpeq12d 5466

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

Syntax hints:   → wi 4   = wceq 1520   × cxp 5433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-12 2139  ax-ext 2767

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1760  df-nf 1764  df-sb 2041  df-clab 2774  df-cleq 2786  df-clel 2861  df-opab 5019  df-xp 5441

This theorem is referenced by:  sqxpeqd  5467  opeliunxp  5497  mpomptsx  7609  dmmpossx  7611  fmpox  7612  ovmptss  7635  fparlem3  7656  fparlem4  7657  erssxp  8153  marypha2lem2  8736  ackbij1lem8  9484  r1om  9501  fictb  9502  axcc2lem  9693  axcc2  9694  axdc4lem  9712  fsum2dlem  14946  fsumcom2  14950  ackbijnn  15004  fprod2dlem  15155  fprodcom2  15159  homaval  17108  xpcval  17244  xpchom  17247  xpchom2  17253  1stfval  17258  2ndfval  17261  xpcpropd  17275  evlfval  17284  isga  18150  symgval  18226  gsumcom2  18803  gsumxp  18804  ablfaclem3  18914  psrval  19818  mamufval  20666  mamudm  20669  mvmulfval  20823  mavmuldm  20831  mavmul0g  20834  txbas  21847  ptbasfi  21861  txindis  21914  tmsxps  22817  metustexhalf  22837  aciunf1lem  30070  fedgmullem1  30584  esum2dlem  30924  lpadval  31520  cvmliftlem15  32109  mexval  32302  mpstval  32335  mclsval  32363  mclsax  32369  mclsppslem  32383  filnetlem4  33283  poimirlem26  34395  poimirlem28  34397  heiborlem3  34569  elrefrels2  35238  refreleq  35241  elcnvrefrels2  35251  dvhfset  37697  dvhset  37698  dibffval  37757  dibfval  37758  hdmap1fval  38413  opeliun2xp  43813  dmmpossx2  43817