Theorem xpeq12d 5685

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

Syntax hints:   → wi 4   = wceq 1540   × cxp 5652

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-opab 5182  df-xp 5660

This theorem is referenced by:  sqxpeqd  5686  opeliunxp  5721  opeliun2xp  5722  mpomptsx  8063  dmmpossx  8065  fmpox  8066  ovmptss  8092  fparlem3  8113  fparlem4  8114  on2recsov  8680  naddcllem  8688  erssxp  8742  marypha2lem2  9448  ackbij1lem8  10240  r1om  10257  fictb  10258  axcc2lem  10450  axcc2  10451  axdc4lem  10469  fsum2dlem  15786  fsumcom2  15790  ackbijnn  15844  fprod2dlem  15996  fprodcom2  16000  homaval  18044  xpcval  18189  xpchom  18192  xpchom2  18198  1stfval  18203  2ndfval  18206  xpcpropd  18220  evlfval  18229  efmnd  18848  isga  19274  gsumcom2  19956  gsumxp  19957  ablfaclem3  20070  psrval  21875  mamufval  22330  mamudm  22333  mvmulfval  22480  mavmuldm  22488  mavmul0g  22491  txbas  23505  ptbasfi  23519  txindis  23572  tmsxps  24475  metustexhalf  24495  noxpordpred  27912  aciunf1lem  32640  gsumpart  33051  gsumwrd2dccatlem  33060  gsumwrd2dccat  33061  erlval  33253  rlocval  33254  fedgmullem1  33669  fldextrspunlsplem  33714  esum2dlem  34123  lpadval  34708  cvmliftlem15  35320  mexval  35524  mpstval  35557  mclsval  35585  mclsax  35591  mclsppslem  35605  filnetlem4  36399  poimirlem26  37670  poimirlem28  37672  heiborlem3  37837  cnvref4  38368  elrefrels2  38536  refreleq  38539  elcnvrefrels2  38552  dvhfset  41099  dvhset  41100  dibffval  41159  dibfval  41160  hdmap1fval  41815  dmmpossx2  48312  dmrnxp  48815  imasubclem3  49065  imaf1hom  49067  swapf2f1oaALT  49195  fucofvalg  49229  fucofvalne  49236  fucof21  49258  functhinclem1  49330  functhinclem3  49332  functhinclem4  49333