Theorem xpeq12d 5683

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

Syntax hints:   → wi 4   = wceq 1563   × cxp 5650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-opab 5168  df-xp 5658

This theorem is referenced by:  sqxpeqd  5684  opeliunxp  5719  opeliun2xp  5720  mpomptsx  8049  dmmpossx  8051  fmpox  8052  ovmptss  8076  fparlem3  8097  fparlem4  8098  on2recsov  8642  naddcllem  8650  erssxp  8706  marypha2lem2  9384  ackbij1lem8  10197  r1om  10214  fictb  10215  axcc2lem  10408  axcc2  10409  axdc4lem  10427  fsum2dlem  15811  fsumcom2  15815  ackbijnn  15872  fprod2dlem  16024  fprodcom2  16028  homaval  18078  xpcval  18223  xpchom  18226  xpchom2  18232  1stfval  18237  2ndfval  18240  xpcpropd  18254  evlfval  18263  efmnd  18919  isga  19352  gsumcom2  20036  gsumxp  20037  ablfaclem3  20150  psrval  22025  mamufval  22510  mamudm  22513  mvmulfval  22660  mavmuldm  22668  mavmul0g  22671  txbas  23685  ptbasfi  23699  txindis  23752  tmsxps  24654  metustexhalf  24674  noxpordpred  28104  aciunf1lem  32919  gsumpart  33296  gsumwrd2dccatlem  33310  gsumwrd2dccat  33311  erlval  33491  rlocval  33492  fedgmullem1  33936  fldextrspunlsplem  33980  esum2dlem  34399  lpadval  34983  cvmliftlem15  35661  mexval  35865  mpstval  35898  mclsval  35926  mclsax  35932  mclsppslem  35946  filnetlem4  36754  poimirlem26  38157  poimirlem28  38159  heiborlem3  38324  cnvref4  38861  elrefrels2  39109  refreleq  39112  elcnvrefrels2  39125  dvhfset  41716  dvhset  41717  dibffval  41776  dibfval  41777  hdmap1fval  42432  dmmpossx2  48968  dmrnxp  49466  imasubclem3  49735  imaf1hom  49737  swapf2f1oaALT  49907  fucofvalg  49947  fucofvalne  49954  fucof21  49976  functhinclem1  50073  functhinclem3  50075  functhinclem4  50076