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

Theorem xpeq12 5561
 Description: Equality theorem for Cartesian product. (Contributed by FL, 31-Aug-2009.)
Assertion
Ref Expression
xpeq12 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴 × 𝐶) = (𝐵 × 𝐷))

Proof of Theorem xpeq12
StepHypRef Expression
1 xpeq1 5550 . 2 (𝐴 = 𝐵 → (𝐴 × 𝐶) = (𝐵 × 𝐶))
2 xpeq2 5557 . 2 (𝐶 = 𝐷 → (𝐵 × 𝐶) = (𝐵 × 𝐷))
31, 2sylan9eq 2879 1 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴 × 𝐶) = (𝐵 × 𝐷))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   × cxp 5534 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-12 2179  ax-ext 2796 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-opab 5110  df-xp 5542 This theorem is referenced by:  xpeq12i  5564  xpeq12d  5567  xpid11  5783  xp11  6013  infxpenlem  9424  fpwwe2lem5  10041  pwfseqlem4a  10068  pwfseqlem4  10069  pwfseqlem5  10070  pwfseq  10071  pwsval  16748  mamufval  20982  mvmulfval  21137  txtopon  22185  txbasval  22200  txindislem  22227  ismet  22919  isxmet  22920  shsval  29084  sat1el2xp  32644  bj-imdirvallem  34500  prdsbnd2  35133  ismgmOLD  35188  opidon2OLD  35192  ttac  39809  rfovd  40535  fsovrfovd  40543  sblpnf  40850
 Copyright terms: Public domain W3C validator