Theorem xpeq12d 5140

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

Syntax hints:   → wi 4   = wceq 1483   × cxp 5112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-opab 4713  df-xp 5120

This theorem is referenced by:  sqxpeqd  5141  opeliunxp  5170  mpt2mptsx  7233  dmmpt2ssx  7235  fmpt2x  7236  ovmptss  7258  fparlem3  7279  fparlem4  7280  erssxp  7765  marypha2lem2  8342  ackbij1lem8  9049  r1om  9066  fictb  9067  axcc2lem  9258  axcc2  9259  axdc4lem  9277  fsum2dlem  14501  fsumcom2  14505  fsumcom2OLD  14506  ackbijnn  14560  fprod2dlem  14710  fprodcom2  14714  fprodcom2OLD  14715  homaval  16681  xpcval  16817  xpchom  16820  xpchom2  16826  1stfval  16831  2ndfval  16834  xpcpropd  16848  evlfval  16857  isga  17724  symgval  17799  gsumcom2  18374  gsumxp  18375  ablfaclem3  18486  psrval  19362  mamufval  20191  mamudm  20194  mvmulfval  20348  mavmuldm  20356  mavmul0g  20359  txbas  21370  ptbasfi  21384  txindis  21437  tmsxps  22341  metustexhalf  22361  aciunf1lem  29462  esum2dlem  30154  cvmliftlem15  31280  mexval  31399  mpstval  31432  mclsval  31460  mclsax  31466  mclsppslem  31480  filnetlem4  32376  poimirlem26  33435  poimirlem28  33437  heiborlem3  33612  dvhfset  36369  dvhset  36370  dibffval  36429  dibfval  36430  hdmap1fval  37086  opeliun2xp  42111  dmmpt2ssx2  42115