Theorem xpeq12d 5682

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

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

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-opab 5168  df-xp 5657

This theorem is used by:  sqxpeqd  5683  opeliunxp  5718  opeliun2xp  5719  mpomptsx  8075  dmmpossx  8077  fmpox  8078  ovmptss  8104  fparlem3  8125  fparlem4  8126  on2recsov  8677  naddcllem  8685  erssxp  8741  marypha2lem2  9428  ackbij1lem8  10304  hfom  10321  fictb  10322  axcc2lem  10514  axcc2  10515  axdc4lem  10533  fsum2dlem  15936  fsumcom2  15940  ackbijnn  15997  fprod2dlem  16147  fprodcom2  16151  homaval  18206  xpcval  18351  xpchom  18354  xpchom2  18360  1stfval  18365  2ndfval  18368  xpcpropd  18382  evlfval  18391  efmnd  19066  isga  19505  gsumcom2  20189  gsumxp  20190  ablfaclem3  20303  psrval  22223  mamufval  22707  mamudm  22710  mvmulfval  22857  mavmuldm  22865  mavmul0g  22868  txbas  23886  ptbasfi  23900  txindis  23953  tmsxps  24855  metustexhalf  24875  noxpordpred  28339  aciunf1lem  33256  gsumpart  33624  gsumwrd2dccatlem  33638  gsumwrd2dccat  33639  erlval  33819  rlocval  33820  fedgmullem1  34261  fldextrspunlsplem  34305  esum2dlem  34724  lpadval  35308  cvmliftlem15  36063  mexval  36267  mpstval  36300  mclsval  36328  mclsax  36334  mclsppslem  36348  filnetlem4  37169  poimirlem26  38564  poimirlem28  38566  heiborlem3  38747  cnvref4  39282  elrefrels2  39530  refreleq  39533  elcnvrefrels2  39546  dvhfset  42137  dvhset  42138  dibffval  42197  dibfval  42198  hdmap1fval  42853  dmmpossx2  49448  dmrnxp  49946  imasubclem3  50213  imaf1hom  50215  swapf2f1oaALT  50385  fucofvalg  50425  fucofvalne  50432  fucof21  50454  functhinclem1  50551  functhinclem3  50553  functhinclem4  50554