Theorem xpeq12d 5619

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-opab 5141  df-xp 5594

This theorem is referenced by:  sqxpeqd  5620  opeliunxp  5653  mpomptsx  7890  dmmpossx  7892  fmpox  7893  ovmptss  7917  fparlem3  7938  fparlem4  7939  erssxp  8495  marypha2lem2  9156  ackbij1lem8  9967  r1om  9984  fictb  9985  axcc2lem  10176  axcc2  10177  axdc4lem  10195  fsum2dlem  15463  fsumcom2  15467  ackbijnn  15521  fprod2dlem  15671  fprodcom2  15675  homaval  17727  xpcval  17875  xpchom  17878  xpchom2  17884  1stfval  17889  2ndfval  17892  xpcpropd  17907  evlfval  17916  efmnd  18490  isga  18878  gsumcom2  19557  gsumxp  19558  ablfaclem3  19671  psrval  21099  mamufval  21515  mamudm  21518  mvmulfval  21672  mavmuldm  21680  mavmul0g  21683  txbas  22699  ptbasfi  22713  txindis  22766  tmsxps  23673  metustexhalf  23693  aciunf1lem  30978  gsumpart  31294  fedgmullem1  31689  esum2dlem  32039  lpadval  32635  cvmliftlem15  33239  mexval  33443  mpstval  33476  mclsval  33504  mclsax  33510  mclsppslem  33524  on2recsov  33806  naddcllem  33810  noxpordpred  34089  filnetlem4  34549  poimirlem26  35782  poimirlem28  35784  heiborlem3  35950  elrefrels2  36614  refreleq  36617  elcnvrefrels2  36627  dvhfset  39073  dvhset  39074  dibffval  39133  dibfval  39134  hdmap1fval  39789  opeliun2xp  45620  dmmpossx2  45624  functhinclem1  46274  functhinclem3  46276  functhinclem4  46277