Theorem xpeq12d 5650

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

Syntax hints:   → wi 4   = wceq 1541   × cxp 5617

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-opab 5156  df-xp 5625

This theorem is referenced by:  sqxpeqd  5651  opeliunxp  5686  opeliun2xp  5687  mpomptsx  8002  dmmpossx  8004  fmpox  8005  ovmptss  8029  fparlem3  8050  fparlem4  8051  on2recsov  8589  naddcllem  8597  erssxp  8651  marypha2lem2  9327  ackbij1lem8  10124  r1om  10141  fictb  10142  axcc2lem  10334  axcc2  10335  axdc4lem  10353  fsum2dlem  15679  fsumcom2  15683  ackbijnn  15737  fprod2dlem  15889  fprodcom2  15893  homaval  17940  xpcval  18085  xpchom  18088  xpchom2  18094  1stfval  18099  2ndfval  18102  xpcpropd  18116  evlfval  18125  efmnd  18780  isga  19205  gsumcom2  19889  gsumxp  19890  ablfaclem3  20003  psrval  21854  mamufval  22308  mamudm  22311  mvmulfval  22458  mavmuldm  22466  mavmul0g  22469  txbas  23483  ptbasfi  23497  txindis  23550  tmsxps  24452  metustexhalf  24472  noxpordpred  27897  aciunf1lem  32646  gsumpart  33044  gsumwrd2dccatlem  33053  gsumwrd2dccat  33054  erlval  33232  rlocval  33233  fedgmullem1  33663  fldextrspunlsplem  33707  esum2dlem  34126  lpadval  34710  cvmliftlem15  35363  mexval  35567  mpstval  35600  mclsval  35628  mclsax  35634  mclsppslem  35648  filnetlem4  36446  poimirlem26  37706  poimirlem28  37708  heiborlem3  37873  cnvref4  38402  elrefrels2  38630  refreleq  38633  elcnvrefrels2  38646  dvhfset  41199  dvhset  41200  dibffval  41259  dibfval  41260  hdmap1fval  41915  dmmpossx2  48461  dmrnxp  48961  imasubclem3  49231  imaf1hom  49233  swapf2f1oaALT  49403  fucofvalg  49443  fucofvalne  49450  fucof21  49472  functhinclem1  49569  functhinclem3  49571  functhinclem4  49572