Theorem xpeq12d 5672

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-opab 5173  df-xp 5647

This theorem is referenced by:  sqxpeqd  5673  opeliunxp  5708  opeliun2xp  5709  mpomptsx  8046  dmmpossx  8048  fmpox  8049  ovmptss  8075  fparlem3  8096  fparlem4  8097  on2recsov  8635  naddcllem  8643  erssxp  8697  marypha2lem2  9394  ackbij1lem8  10186  r1om  10203  fictb  10204  axcc2lem  10396  axcc2  10397  axdc4lem  10415  fsum2dlem  15743  fsumcom2  15747  ackbijnn  15801  fprod2dlem  15953  fprodcom2  15957  homaval  18000  xpcval  18145  xpchom  18148  xpchom2  18154  1stfval  18159  2ndfval  18162  xpcpropd  18176  evlfval  18185  efmnd  18804  isga  19230  gsumcom2  19912  gsumxp  19913  ablfaclem3  20026  psrval  21831  mamufval  22286  mamudm  22289  mvmulfval  22436  mavmuldm  22444  mavmul0g  22447  txbas  23461  ptbasfi  23475  txindis  23528  tmsxps  24431  metustexhalf  24451  noxpordpred  27867  aciunf1lem  32593  gsumpart  33004  gsumwrd2dccatlem  33013  gsumwrd2dccat  33014  erlval  33216  rlocval  33217  fedgmullem1  33632  fldextrspunlsplem  33675  esum2dlem  34089  lpadval  34674  cvmliftlem15  35292  mexval  35496  mpstval  35529  mclsval  35557  mclsax  35563  mclsppslem  35577  filnetlem4  36376  poimirlem26  37647  poimirlem28  37649  heiborlem3  37814  cnvref4  38339  elrefrels2  38516  refreleq  38519  elcnvrefrels2  38532  dvhfset  41081  dvhset  41082  dibffval  41141  dibfval  41142  hdmap1fval  41797  dmmpossx2  48329  dmrnxp  48829  imasubclem3  49099  imaf1hom  49101  swapf2f1oaALT  49271  fucofvalg  49311  fucofvalne  49318  fucof21  49340  functhinclem1  49437  functhinclem3  49439  functhinclem4  49440