Theorem xpeq12d 5705

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

Syntax hints:   → wi 4   = wceq 1534   × cxp 5672

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-opab 5208  df-xp 5680

This theorem is referenced by:  sqxpeqd  5706  opeliunxp  5741  mpomptsx  8070  dmmpossx  8072  fmpox  8073  ovmptss  8099  fparlem3  8120  fparlem4  8121  on2recsov  8690  naddcllem  8698  erssxp  8749  marypha2lem2  9472  ackbij1lem8  10261  r1om  10278  fictb  10279  axcc2lem  10470  axcc2  10471  axdc4lem  10489  fsum2dlem  15769  fsumcom2  15773  ackbijnn  15827  fprod2dlem  15977  fprodcom2  15981  homaval  18048  xpcval  18196  xpchom  18199  xpchom2  18205  1stfval  18210  2ndfval  18213  xpcpropd  18228  evlfval  18237  efmnd  18855  isga  19281  gsumcom2  19969  gsumxp  19970  ablfaclem3  20083  psrval  21908  mamufval  22380  mamudm  22383  mvmulfval  22532  mavmuldm  22540  mavmul0g  22543  txbas  23559  ptbasfi  23573  txindis  23626  tmsxps  24533  metustexhalf  24553  noxpordpred  27964  aciunf1lem  32579  gsumpart  32927  erlval  33118  rlocval  33119  fedgmullem1  33530  esum2dlem  33938  lpadval  34535  cvmliftlem15  35139  mexval  35343  mpstval  35376  mclsval  35404  mclsax  35410  mclsppslem  35424  filnetlem4  36106  poimirlem26  37360  poimirlem28  37362  heiborlem3  37527  cnvref4  38061  elrefrels2  38229  refreleq  38232  elcnvrefrels2  38245  dvhfset  40792  dvhset  40793  dibffval  40852  dibfval  40853  hdmap1fval  41508  opeliun2xp  47747  dmmpossx2  47751  functhinclem1  48398  functhinclem3  48400  functhinclem4  48401