Theorem xpeq12d 5694

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

Syntax hints:   → wi 4   = wceq 1570   × cxp 5661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-opab 5175  df-xp 5669

This theorem is referenced by:  sqxpeqd  5695  opeliunxp  5730  opeliun2xp  5731  mpomptsx  8062  dmmpossx  8064  fmpox  8065  ovmptss  8089  fparlem3  8110  fparlem4  8111  on2recsov  8655  naddcllem  8663  erssxp  8719  marypha2lem2  9397  ackbij1lem8  10210  r1om  10227  fictb  10228  axcc2lem  10421  axcc2  10422  axdc4lem  10440  fsum2dlem  15823  fsumcom2  15827  ackbijnn  15884  fprod2dlem  16036  fprodcom2  16040  homaval  18089  xpcval  18234  xpchom  18237  xpchom2  18243  1stfval  18248  2ndfval  18251  xpcpropd  18265  evlfval  18274  efmnd  18930  isga  19362  gsumcom2  20046  gsumxp  20047  ablfaclem3  20160  psrval  22046  mamufval  22530  mamudm  22533  mvmulfval  22680  mavmuldm  22688  mavmul0g  22691  txbas  23705  ptbasfi  23719  txindis  23772  tmsxps  24674  metustexhalf  24694  noxpordpred  28127  aciunf1lem  32988  gsumpart  33364  gsumwrd2dccatlem  33378  gsumwrd2dccat  33379  erlval  33559  rlocval  33560  fedgmullem1  34000  fldextrspunlsplem  34044  esum2dlem  34463  lpadval  35047  cvmliftlem15  35771  mexval  35975  mpstval  36008  mclsval  36036  mclsax  36042  mclsppslem  36056  filnetlem4  36873  poimirlem26  38278  poimirlem28  38280  heiborlem3  38445  cnvref4  38980  elrefrels2  39228  refreleq  39231  elcnvrefrels2  39244  dvhfset  41835  dvhset  41836  dibffval  41895  dibfval  41896  hdmap1fval  42551  dmmpossx2  49100  dmrnxp  49598  imasubclem3  49867  imaf1hom  49869  swapf2f1oaALT  50039  fucofvalg  50079  fucofvalne  50086  fucof21  50108  functhinclem1  50205  functhinclem3  50207  functhinclem4  50208