Theorem xpeq12d 5280

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

Syntax hints:   → wi 4   = wceq 1631   × cxp 5247

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-opab 4847  df-xp 5255

This theorem is referenced by:  sqxpeqd  5281  opeliunxp  5310  mpt2mptsx  7383  dmmpt2ssx  7385  fmpt2x  7386  ovmptss  7409  fparlem3  7430  fparlem4  7431  erssxp  7919  marypha2lem2  8498  ackbij1lem8  9251  r1om  9268  fictb  9269  axcc2lem  9460  axcc2  9461  axdc4lem  9479  fsum2dlem  14709  fsumcom2  14713  ackbijnn  14767  fprod2dlem  14917  fprodcom2  14921  homaval  16888  xpcval  17025  xpchom  17028  xpchom2  17034  1stfval  17039  2ndfval  17042  xpcpropd  17056  evlfval  17065  isga  17931  symgval  18006  gsumcom2  18581  gsumxp  18582  ablfaclem3  18694  psrval  19577  mamufval  20408  mamudm  20411  mvmulfval  20566  mavmuldm  20574  mavmul0g  20577  txbas  21591  ptbasfi  21605  txindis  21658  tmsxps  22561  metustexhalf  22581  aciunf1lem  29802  esum2dlem  30494  cvmliftlem15  31618  mexval  31737  mpstval  31770  mclsval  31798  mclsax  31804  mclsppslem  31818  filnetlem4  32713  poimirlem26  33768  poimirlem28  33770  heiborlem3  33944  elrefrels2  34609  refreleq  34612  elcnvrefrels2  34622  dvhfset  36890  dvhset  36891  dibffval  36950  dibfval  36951  hdmap1fval  37606  opeliun2xp  42639  dmmpt2ssx2  42643