MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xpeq12d Structured version   Visualization version   GIF version

Theorem xpeq12d 5105
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
StepHypRef Expression
1 xpeq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 xpeq12d.2 . 2 (𝜑𝐶 = 𝐷)
3 xpeq12 5099 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴 × 𝐶) = (𝐵 × 𝐷))
41, 2, 3syl2anc 692 1 (𝜑 → (𝐴 × 𝐶) = (𝐵 × 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480   × cxp 5077
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-opab 4679  df-xp 5085
This theorem is referenced by:  sqxpeqd  5106  opeliunxp  5136  mpt2mptsx  7185  dmmpt2ssx  7187  fmpt2x  7188  ovmptss  7210  fparlem3  7231  fparlem4  7232  erssxp  7717  marypha2lem2  8293  ackbij1lem8  9000  r1om  9017  fictb  9018  axcc2lem  9209  axcc2  9210  axdc4lem  9228  fsum2dlem  14436  fsumcom2  14440  fsumcom2OLD  14441  ackbijnn  14492  fprod2dlem  14642  fprodcom2  14646  fprodcom2OLD  14647  homaval  16609  xpcval  16745  xpchom  16748  xpchom2  16754  1stfval  16759  2ndfval  16762  xpcpropd  16776  evlfval  16785  isga  17652  symgval  17727  gsumcom2  18302  gsumxp  18303  ablfaclem3  18414  psrval  19290  mamufval  20119  mamudm  20122  mvmulfval  20276  mavmuldm  20284  mavmul0g  20287  txbas  21289  ptbasfi  21303  txindis  21356  tmsxps  22260  metustexhalf  22280  aciunf1lem  29322  esum2dlem  29953  cvmliftlem15  31015  mexval  31134  mpstval  31167  mclsval  31195  mclsax  31201  mclsppslem  31215  filnetlem4  32045  poimirlem26  33094  poimirlem28  33096  heiborlem3  33271  dvhfset  35876  dvhset  35877  dibffval  35936  dibfval  35937  hdmap1fval  36593  opeliun2xp  41420  dmmpt2ssx2  41424
  Copyright terms: Public domain W3C validator