Theorem xpeq12d 5582

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

Syntax hints:   → wi 4   = wceq 1543   × cxp 5549

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-opab 5116  df-xp 5557

This theorem is referenced by:  sqxpeqd  5583  opeliunxp  5616  mpomptsx  7834  dmmpossx  7836  fmpox  7837  ovmptss  7861  fparlem3  7882  fparlem4  7883  erssxp  8414  marypha2lem2  9052  ackbij1lem8  9841  r1om  9858  fictb  9859  axcc2lem  10050  axcc2  10051  axdc4lem  10069  fsum2dlem  15334  fsumcom2  15338  ackbijnn  15392  fprod2dlem  15542  fprodcom2  15546  homaval  17537  xpcval  17684  xpchom  17687  xpchom2  17693  1stfval  17698  2ndfval  17701  xpcpropd  17716  evlfval  17725  efmnd  18297  isga  18685  gsumcom2  19360  gsumxp  19361  ablfaclem3  19474  psrval  20874  mamufval  21284  mamudm  21287  mvmulfval  21439  mavmuldm  21447  mavmul0g  21450  txbas  22464  ptbasfi  22478  txindis  22531  tmsxps  23434  metustexhalf  23454  aciunf1lem  30719  gsumpart  31034  fedgmullem1  31424  esum2dlem  31772  lpadval  32368  cvmliftlem15  32973  mexval  33177  mpstval  33210  mclsval  33238  mclsax  33244  mclsppslem  33258  on2recsov  33564  naddcllem  33568  noxpordpred  33847  filnetlem4  34307  poimirlem26  35540  poimirlem28  35542  heiborlem3  35708  elrefrels2  36372  refreleq  36375  elcnvrefrels2  36385  dvhfset  38831  dvhset  38832  dibffval  38891  dibfval  38892  hdmap1fval  39547  opeliun2xp  45341  dmmpossx2  45345  functhinclem1  45995  functhinclem3  45997  functhinclem4  45998