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

Theorem xpeq12d 5064
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 5058 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴 × 𝐶) = (𝐵 × 𝐷))
41, 2, 3syl2anc 691 1 (𝜑 → (𝐴 × 𝐶) = (𝐵 × 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1475   × cxp 5036
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-opab 4644  df-xp 5044
This theorem is referenced by:  sqxpeqd  5065  opeliunxp  5093  mpt2mptsx  7122  dmmpt2ssx  7124  fmpt2x  7125  ovmptss  7145  fparlem3  7166  fparlem4  7167  erssxp  7652  marypha2lem2  8225  ackbij1lem8  8932  r1om  8949  fictb  8950  axcc2lem  9141  axcc2  9142  axdc4lem  9160  fsum2dlem  14343  fsumcom2  14347  fsumcom2OLD  14348  ackbijnn  14399  fprod2dlem  14549  fprodcom2  14553  fprodcom2OLD  14554  homaval  16504  xpcval  16640  xpchom  16643  xpchom2  16649  1stfval  16654  2ndfval  16657  xpcpropd  16671  evlfval  16680  isga  17547  symgval  17622  gsumcom2  18197  gsumxp  18198  ablfaclem3  18309  psrval  19183  mamufval  20010  mamudm  20013  mvmulfval  20167  mavmuldm  20175  mavmul0g  20178  txbas  21180  ptbasfi  21194  txindis  21247  tmsxps  22151  metustexhalf  22171  is2wlkonot  26390  is2spthonot  26391  2wlksot  26394  2spthsot  26395  2wlkonot3v  26402  2spthonot3v  26403  aciunf1lem  28844  esum2dlem  29481  cvmliftlem15  30534  mexval  30653  mpstval  30686  mclsval  30714  mclsax  30720  mclsppslem  30734  filnetlem4  31546  poimirlem26  32605  poimirlem28  32607  heiborlem3  32782  dvhfset  35387  dvhset  35388  dibffval  35447  dibfval  35448  hdmap1fval  36104  opeliun2xp  41904  dmmpt2ssx2  41908
  Copyright terms: Public domain W3C validator