Theorem xpeq12d 5669

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

Syntax hints:   → wi 4   = wceq 1540   × cxp 5636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-opab 5170  df-xp 5644

This theorem is referenced by:  sqxpeqd  5670  opeliunxp  5705  opeliun2xp  5706  mpomptsx  8043  dmmpossx  8045  fmpox  8046  ovmptss  8072  fparlem3  8093  fparlem4  8094  on2recsov  8632  naddcllem  8640  erssxp  8694  marypha2lem2  9387  ackbij1lem8  10179  r1om  10196  fictb  10197  axcc2lem  10389  axcc2  10390  axdc4lem  10408  fsum2dlem  15736  fsumcom2  15740  ackbijnn  15794  fprod2dlem  15946  fprodcom2  15950  homaval  17993  xpcval  18138  xpchom  18141  xpchom2  18147  1stfval  18152  2ndfval  18155  xpcpropd  18169  evlfval  18178  efmnd  18797  isga  19223  gsumcom2  19905  gsumxp  19906  ablfaclem3  20019  psrval  21824  mamufval  22279  mamudm  22282  mvmulfval  22429  mavmuldm  22437  mavmul0g  22440  txbas  23454  ptbasfi  23468  txindis  23521  tmsxps  24424  metustexhalf  24444  noxpordpred  27860  aciunf1lem  32586  gsumpart  32997  gsumwrd2dccatlem  33006  gsumwrd2dccat  33007  erlval  33209  rlocval  33210  fedgmullem1  33625  fldextrspunlsplem  33668  esum2dlem  34082  lpadval  34667  cvmliftlem15  35285  mexval  35489  mpstval  35522  mclsval  35550  mclsax  35556  mclsppslem  35570  filnetlem4  36369  poimirlem26  37640  poimirlem28  37642  heiborlem3  37807  cnvref4  38332  elrefrels2  38509  refreleq  38512  elcnvrefrels2  38525  dvhfset  41074  dvhset  41075  dibffval  41134  dibfval  41135  hdmap1fval  41790  dmmpossx2  48325  dmrnxp  48825  imasubclem3  49095  imaf1hom  49097  swapf2f1oaALT  49267  fucofvalg  49307  fucofvalne  49314  fucof21  49336  functhinclem1  49433  functhinclem3  49435  functhinclem4  49436