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

Theorem xpeq12d 5708
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 5702 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴 × 𝐶) = (𝐵 × 𝐷))
41, 2, 3syl2anc 585 1 (𝜑 → (𝐴 × 𝐶) = (𝐵 × 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542   × cxp 5675
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-opab 5212  df-xp 5683
This theorem is referenced by:  sqxpeqd  5709  opeliunxp  5744  mpomptsx  8050  dmmpossx  8052  fmpox  8053  ovmptss  8079  fparlem3  8100  fparlem4  8101  on2recsov  8667  naddcllem  8675  erssxp  8726  marypha2lem2  9431  ackbij1lem8  10222  r1om  10239  fictb  10240  axcc2lem  10431  axcc2  10432  axdc4lem  10450  fsum2dlem  15716  fsumcom2  15720  ackbijnn  15774  fprod2dlem  15924  fprodcom2  15928  homaval  17981  xpcval  18129  xpchom  18132  xpchom2  18138  1stfval  18143  2ndfval  18146  xpcpropd  18161  evlfval  18170  efmnd  18751  isga  19155  gsumcom2  19843  gsumxp  19844  ablfaclem3  19957  psrval  21468  mamufval  21887  mamudm  21890  mvmulfval  22044  mavmuldm  22052  mavmul0g  22055  txbas  23071  ptbasfi  23085  txindis  23138  tmsxps  24045  metustexhalf  24065  noxpordpred  27439  aciunf1lem  31918  gsumpart  32238  fedgmullem1  32745  esum2dlem  33121  lpadval  33719  cvmliftlem15  34320  mexval  34524  mpstval  34557  mclsval  34585  mclsax  34591  mclsppslem  34605  filnetlem4  35314  poimirlem26  36562  poimirlem28  36564  heiborlem3  36729  cnvref4  37267  elrefrels2  37436  refreleq  37439  elcnvrefrels2  37452  dvhfset  39999  dvhset  40000  dibffval  40059  dibfval  40060  hdmap1fval  40715  opeliun2xp  47056  dmmpossx2  47060  functhinclem1  47709  functhinclem3  47711  functhinclem4  47712
  Copyright terms: Public domain W3C validator