Theorem xpeq12d 5687

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-opab 5172  df-xp 5662

This theorem is used by:  sqxpeqd  5688  opeliunxp  5723  opeliun2xp  5724  mpomptsx  8103  dmmpossx  8105  fmpox  8106  ovmptssOLD  8133  fparlem3  8155  fparlem4  8156  on2recsov  8708  naddcllem  8716  erssxp  8772  marypha2lem2  9458  ackbij1lem8  10334  hfom  10351  fictb  10352  axcc2lem  10544  axcc2  10545  axdc4lem  10563  fsum2dlem  15968  fsumcom2  15972  ackbijnn  16029  fprod2dlem  16179  fprodcom2  16183  homaval  18238  xpcval  18383  xpchom  18386  xpchom2  18392  1stfval  18397  2ndfval  18400  xpcpropd  18414  evlfval  18423  efmnd  19098  isga  19538  gsumcom2  20222  gsumxp  20223  ablfaclem3  20336  psrval  22256  mamufval  22740  mamudm  22743  mvmulfval  22890  mavmuldm  22898  mavmul0g  22901  txbas  23919  ptbasfi  23933  txindis  23986  tmsxps  24888  metustexhalf  24908  noxpordpred  28372  aciunf1lem  33331  gsumpart  33700  gsumwrd2dccatlem  33714  gsumwrd2dccat  33715  erlval  33895  rlocval  33896  fedgmullem1  34344  fldextrspunlsplem  34388  esum2dlem  34807  lpadval  35391  cvmliftlem15  36243  mexval  36447  mpstval  36480  mclsval  36508  mclsax  36514  mclsppslem  36528  filnetlem4  37360  poimirlem26  38769  poimirlem28  38771  heiborlem3  38950  cnvref4  39485  elrefrels2  39733  refreleq  39736  elcnvrefrels2  39749  dvhfset  42340  dvhset  42341  dibffval  42400  dibfval  42401  hdmap1fval  43056  ackbij3  46231  dmmpossx2  49664  dmrnxp  50163  imasubclem3  50437  imaf1hom  50439  swapf2f1oaALT  50615  fucofvalg  50655  fucofvalne  50662  fucof21  50684  functhinclem1  50794  functhinclem3  50796  functhinclem4  50797