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

Theorem xpeq12d 5580
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 5574 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴 × 𝐶) = (𝐵 × 𝐷))
41, 2, 3syl2anc 584 1 (𝜑 → (𝐴 × 𝐶) = (𝐵 × 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528   × cxp 5547
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-opab 5121  df-xp 5555
This theorem is referenced by:  sqxpeqd  5581  opeliunxp  5613  mpomptsx  7753  dmmpossx  7755  fmpox  7756  ovmptss  7779  fparlem3  7800  fparlem4  7801  erssxp  8302  marypha2lem2  8889  ackbij1lem8  9638  r1om  9655  fictb  9656  axcc2lem  9847  axcc2  9848  axdc4lem  9866  fsum2dlem  15115  fsumcom2  15119  ackbijnn  15173  fprod2dlem  15324  fprodcom2  15328  homaval  17281  xpcval  17417  xpchom  17420  xpchom2  17426  1stfval  17431  2ndfval  17434  xpcpropd  17448  evlfval  17457  isga  18361  symgval  18437  gsumcom2  19026  gsumxp  19027  ablfaclem3  19140  psrval  20072  mamufval  20926  mamudm  20929  mvmulfval  21081  mavmuldm  21089  mavmul0g  21092  txbas  22105  ptbasfi  22119  txindis  22172  tmsxps  23075  metustexhalf  23095  aciunf1lem  30336  fedgmullem1  30925  esum2dlem  31251  lpadval  31847  cvmliftlem15  32443  mexval  32647  mpstval  32680  mclsval  32708  mclsax  32714  mclsppslem  32728  filnetlem4  33627  poimirlem26  34800  poimirlem28  34802  heiborlem3  34974  elrefrels2  35639  refreleq  35642  elcnvrefrels2  35652  dvhfset  38098  dvhset  38099  dibffval  38158  dibfval  38159  hdmap1fval  38814  efmnd  43939  opeliun2xp  44279  dmmpossx2  44283
  Copyright terms: Public domain W3C validator