Theorem xpeq12d 5655

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

Syntax hints:   → wi 4   = wceq 1542   × cxp 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-opab 5149  df-xp 5630

This theorem is referenced by:  sqxpeqd  5656  opeliunxp  5691  opeliun2xp  5692  mpomptsx  8010  dmmpossx  8012  fmpox  8013  ovmptss  8036  fparlem3  8057  fparlem4  8058  on2recsov  8597  naddcllem  8605  erssxp  8660  marypha2lem2  9342  ackbij1lem8  10139  r1om  10156  fictb  10157  axcc2lem  10349  axcc2  10350  axdc4lem  10368  fsum2dlem  15723  fsumcom2  15727  ackbijnn  15784  fprod2dlem  15936  fprodcom2  15940  homaval  17989  xpcval  18134  xpchom  18137  xpchom2  18143  1stfval  18148  2ndfval  18151  xpcpropd  18165  evlfval  18174  efmnd  18829  isga  19257  gsumcom2  19941  gsumxp  19942  ablfaclem3  20055  psrval  21905  mamufval  22367  mamudm  22370  mvmulfval  22517  mavmuldm  22525  mavmul0g  22528  txbas  23542  ptbasfi  23556  txindis  23609  tmsxps  24511  metustexhalf  24531  noxpordpred  27959  aciunf1lem  32750  gsumpart  33139  gsumwrd2dccatlem  33153  gsumwrd2dccat  33154  erlval  33334  rlocval  33335  fedgmullem1  33789  fldextrspunlsplem  33833  esum2dlem  34252  lpadval  34836  cvmliftlem15  35496  mexval  35700  mpstval  35733  mclsval  35761  mclsax  35767  mclsppslem  35781  filnetlem4  36579  poimirlem26  37981  poimirlem28  37983  heiborlem3  38148  cnvref4  38685  elrefrels2  38933  refreleq  38936  elcnvrefrels2  38949  dvhfset  41540  dvhset  41541  dibffval  41600  dibfval  41601  hdmap1fval  42256  dmmpossx2  48825  dmrnxp  49324  imasubclem3  49593  imaf1hom  49595  swapf2f1oaALT  49765  fucofvalg  49805  fucofvalne  49812  fucof21  49834  functhinclem1  49931  functhinclem3  49933  functhinclem4  49934