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 1541   × cxp 5636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-opab 5173  df-xp 5644

This theorem is referenced by:  sqxpeqd  5670  opeliunxp  5704  mpomptsx  8001  dmmpossx  8003  fmpox  8004  ovmptss  8030  fparlem3  8051  fparlem4  8052  on2recsov  8619  naddcllem  8627  erssxp  8678  marypha2lem2  9381  ackbij1lem8  10172  r1om  10189  fictb  10190  axcc2lem  10381  axcc2  10382  axdc4lem  10400  fsum2dlem  15666  fsumcom2  15670  ackbijnn  15724  fprod2dlem  15874  fprodcom2  15878  homaval  17931  xpcval  18079  xpchom  18082  xpchom2  18088  1stfval  18093  2ndfval  18096  xpcpropd  18111  evlfval  18120  efmnd  18694  isga  19085  gsumcom2  19766  gsumxp  19767  ablfaclem3  19880  psrval  21354  mamufval  21771  mamudm  21774  mvmulfval  21928  mavmuldm  21936  mavmul0g  21939  txbas  22955  ptbasfi  22969  txindis  23022  tmsxps  23929  metustexhalf  23949  noxpordpred  27308  aciunf1lem  31645  gsumpart  31967  fedgmullem1  32411  esum2dlem  32780  lpadval  33378  cvmliftlem15  33979  mexval  34183  mpstval  34216  mclsval  34244  mclsax  34250  mclsppslem  34264  filnetlem4  34929  poimirlem26  36177  poimirlem28  36179  heiborlem3  36345  cnvref4  36884  elrefrels2  37053  refreleq  37056  elcnvrefrels2  37069  dvhfset  39616  dvhset  39617  dibffval  39676  dibfval  39677  hdmap1fval  40332  opeliun2xp  46528  dmmpossx2  46532  functhinclem1  47181  functhinclem3  47183  functhinclem4  47184