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

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

Proof of Theorem xpeq12
StepHypRef Expression
1 xpeq1 5052 . 2 (𝐴 = 𝐵 → (𝐴 × 𝐶) = (𝐵 × 𝐶))
2 xpeq2 5053 . 2 (𝐶 = 𝐷 → (𝐵 × 𝐶) = (𝐵 × 𝐷))
31, 2sylan9eq 2664 1 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴 × 𝐶) = (𝐵 × 𝐷))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   = 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:  xpeq12i  5061  xpeq12d  5064  xpid11  5268  xp11  5488  infxpenlem  8719  fpwwe2lem5  9335  pwfseqlem4a  9362  pwfseqlem4  9363  pwfseqlem5  9364  pwfseq  9365  pwsval  15969  mamufval  20010  mvmulfval  20167  txtopon  21204  txbasval  21219  txindislem  21246  ismet  21938  isxmet  21939  shsval  27555  prdsbnd2  32764  ismgmOLD  32819  opidon2OLD  32823  ttac  36621  rfovd  37315  fsovrfovd  37323  sblpnf  37531
 Copyright terms: Public domain W3C validator