Theorem xpeq12d 5647

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

Syntax hints:   → wi 4   = wceq 1541   × cxp 5614

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-opab 5154  df-xp 5622

This theorem is referenced by:  sqxpeqd  5648  opeliunxp  5683  opeliun2xp  5684  mpomptsx  7996  dmmpossx  7998  fmpox  7999  ovmptss  8023  fparlem3  8044  fparlem4  8045  on2recsov  8583  naddcllem  8591  erssxp  8645  marypha2lem2  9320  ackbij1lem8  10114  r1om  10131  fictb  10132  axcc2lem  10324  axcc2  10325  axdc4lem  10343  fsum2dlem  15674  fsumcom2  15678  ackbijnn  15732  fprod2dlem  15884  fprodcom2  15888  homaval  17935  xpcval  18080  xpchom  18083  xpchom2  18089  1stfval  18094  2ndfval  18097  xpcpropd  18111  evlfval  18120  efmnd  18775  isga  19201  gsumcom2  19885  gsumxp  19886  ablfaclem3  19999  psrval  21850  mamufval  22305  mamudm  22308  mvmulfval  22455  mavmuldm  22463  mavmul0g  22466  txbas  23480  ptbasfi  23494  txindis  23547  tmsxps  24449  metustexhalf  24469  noxpordpred  27894  aciunf1lem  32639  gsumpart  33032  gsumwrd2dccatlem  33041  gsumwrd2dccat  33042  erlval  33220  rlocval  33221  fedgmullem1  33637  fldextrspunlsplem  33681  esum2dlem  34100  lpadval  34684  cvmliftlem15  35330  mexval  35534  mpstval  35567  mclsval  35595  mclsax  35601  mclsppslem  35615  filnetlem4  36414  poimirlem26  37685  poimirlem28  37687  heiborlem3  37852  cnvref4  38377  elrefrels2  38554  refreleq  38557  elcnvrefrels2  38570  dvhfset  41118  dvhset  41119  dibffval  41178  dibfval  41179  hdmap1fval  41834  dmmpossx2  48367  dmrnxp  48867  imasubclem3  49137  imaf1hom  49139  swapf2f1oaALT  49309  fucofvalg  49349  fucofvalne  49356  fucof21  49378  functhinclem1  49475  functhinclem3  49477  functhinclem4  49478