Theorem xpeq12d 5682

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   × cxp 5649

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-opab 5168  df-xp 5657

This theorem is used by:  sqxpeqd  5683  opeliunxp  5718  opeliun2xp  5719  mpomptsx  8064  dmmpossx  8066  fmpox  8067  ovmptss  8093  fparlem3  8114  fparlem4  8115  on2recsov  8661  naddcllem  8669  erssxp  8725  marypha2lem2  9412  ackbij1lem8  10285  hfom  10302  fictb  10303  axcc2lem  10495  axcc2  10496  axdc4lem  10514  fsum2dlem  15916  fsumcom2  15920  ackbijnn  15977  fprod2dlem  16127  fprodcom2  16131  homaval  18186  xpcval  18331  xpchom  18334  xpchom2  18340  1stfval  18345  2ndfval  18348  xpcpropd  18362  evlfval  18371  efmnd  19046  isga  19485  gsumcom2  20169  gsumxp  20170  ablfaclem3  20283  psrval  22203  mamufval  22687  mamudm  22690  mvmulfval  22837  mavmuldm  22845  mavmul0g  22848  txbas  23866  ptbasfi  23880  txindis  23933  tmsxps  24835  metustexhalf  24855  noxpordpred  28321  aciunf1lem  33238  gsumpart  33606  gsumwrd2dccatlem  33620  gsumwrd2dccat  33621  erlval  33801  rlocval  33802  fedgmullem1  34243  fldextrspunlsplem  34287  esum2dlem  34706  lpadval  35291  cvmliftlem15  36032  mexval  36236  mpstval  36269  mclsval  36297  mclsax  36303  mclsppslem  36317  filnetlem4  37139  poimirlem26  38532  poimirlem28  38534  heiborlem3  38715  cnvref4  39250  elrefrels2  39498  refreleq  39501  elcnvrefrels2  39514  dvhfset  42105  dvhset  42106  dibffval  42165  dibfval  42166  hdmap1fval  42821  dmmpossx2  49393  dmrnxp  49891  imasubclem3  50158  imaf1hom  50160  swapf2f1oaALT  50330  fucofvalg  50370  fucofvalne  50377  fucof21  50399  functhinclem1  50496  functhinclem3  50498  functhinclem4  50499