Theorem xpeq12d 5690

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   × cxp 5657

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-opab 5172  df-xp 5665

This theorem is used by:  sqxpeqd  5691  opeliunxp  5726  opeliun2xp  5727  mpomptsx  8065  dmmpossx  8067  fmpox  8068  ovmptss  8094  fparlem3  8115  fparlem4  8116  on2recsov  8660  naddcllem  8668  erssxp  8724  marypha2lem2  9410  ackbij1lem8  10232  r1om  10249  fictb  10250  axcc2lem  10442  axcc2  10443  axdc4lem  10461  fsum2dlem  15860  fsumcom2  15864  ackbijnn  15921  fprod2dlem  16073  fprodcom2  16077  homaval  18126  xpcval  18271  xpchom  18274  xpchom2  18280  1stfval  18285  2ndfval  18288  xpcpropd  18302  evlfval  18311  efmnd  18985  isga  19424  gsumcom2  20108  gsumxp  20109  ablfaclem3  20222  psrval  22136  mamufval  22620  mamudm  22623  mvmulfval  22770  mavmuldm  22778  mavmul0g  22781  txbas  23799  ptbasfi  23813  txindis  23866  tmsxps  24768  metustexhalf  24788  noxpordpred  28226  aciunf1lem  33143  gsumpart  33511  gsumwrd2dccatlem  33525  gsumwrd2dccat  33526  erlval  33706  rlocval  33707  fedgmullem1  34147  fldextrspunlsplem  34191  esum2dlem  34610  lpadval  35195  cvmliftlem15  35885  mexval  36089  mpstval  36122  mclsval  36150  mclsax  36156  mclsppslem  36170  filnetlem4  37008  poimirlem26  38403  poimirlem28  38405  heiborlem3  38571  cnvref4  39106  elrefrels2  39354  refreleq  39357  elcnvrefrels2  39370  dvhfset  41961  dvhset  41962  dibffval  42021  dibfval  42022  hdmap1fval  42677  dmmpossx2  49275  dmrnxp  49773  imasubclem3  50040  imaf1hom  50042  swapf2f1oaALT  50212  fucofvalg  50252  fucofvalne  50259  fucof21  50281  functhinclem1  50378  functhinclem3  50380  functhinclem4  50381