Theorem xpeq12d 5681

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   × cxp 5648

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-opab 5167  df-xp 5656

This theorem is used by:  sqxpeqd  5682  opeliunxp  5717  opeliun2xp  5718  mpomptsx  8075  dmmpossx  8077  fmpox  8078  ovmptssOLD  8105  fparlem3  8127  fparlem4  8128  on2recsov  8680  naddcllem  8688  erssxp  8744  marypha2lem2  9431  ackbij1lem8  10307  hfom  10324  fictb  10325  axcc2lem  10517  axcc2  10518  axdc4lem  10536  fsum2dlem  15941  fsumcom2  15945  ackbijnn  16002  fprod2dlem  16152  fprodcom2  16156  homaval  18211  xpcval  18356  xpchom  18359  xpchom2  18365  1stfval  18370  2ndfval  18373  xpcpropd  18387  evlfval  18396  efmnd  19071  isga  19510  gsumcom2  20194  gsumxp  20195  ablfaclem3  20308  psrval  22228  mamufval  22712  mamudm  22715  mvmulfval  22862  mavmuldm  22870  mavmul0g  22873  txbas  23891  ptbasfi  23905  txindis  23958  tmsxps  24860  metustexhalf  24880  noxpordpred  28344  aciunf1lem  33303  gsumpart  33670  gsumwrd2dccatlem  33684  gsumwrd2dccat  33685  erlval  33865  rlocval  33866  fedgmullem1  34307  fldextrspunlsplem  34351  esum2dlem  34770  lpadval  35354  cvmliftlem15  36149  mexval  36353  mpstval  36386  mclsval  36414  mclsax  36420  mclsppslem  36434  filnetlem4  37261  poimirlem26  38657  poimirlem28  38659  heiborlem3  38840  cnvref4  39375  elrefrels2  39623  refreleq  39626  elcnvrefrels2  39639  dvhfset  42230  dvhset  42231  dibffval  42290  dibfval  42291  hdmap1fval  42946  dmmpossx2  49542  dmrnxp  50041  imasubclem3  50315  imaf1hom  50317  swapf2f1oaALT  50493  fucofvalg  50533  fucofvalne  50540  fucof21  50562  functhinclem1  50672  functhinclem3  50674  functhinclem4  50675