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

Theorem xpeq12 4710
Description: Equality theorem for cross product. (Contributed by FL, 31-Aug-2009.)
Assertion
Ref Expression
xpeq12  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  X.  C
)  =  ( B  X.  D ) )

Proof of Theorem xpeq12
StepHypRef Expression
1 xpeq1 4705 . 2  |-  ( A  =  B  ->  ( A  X.  C )  =  ( B  X.  C
) )
2 xpeq2 4706 . 2  |-  ( C  =  D  ->  ( B  X.  C )  =  ( B  X.  D
) )
31, 2sylan9eq 2337 1  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  X.  C
)  =  ( B  X.  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1625    X. cxp 4689
This theorem is referenced by:  xpeq12i  4713  xpeq12d  4716  xpid11  4902  xp11  5113  infxpenlem  7643  fpwwe2lem5  8258  pwfseqlem4a  8285  pwfseqlem4  8286  pwfseqlem5  8287  pwfseq  8288  pwsval  13387  txtopon  17288  txbasval  17303  txindislem  17329  ismet  17890  isxmet  17891  ismgm  20989  opidon2  20993  shsval  21893  relinccppr  25140  islatalg  25194  domrancur1c  25213  svs2  25498  prdsbnd2  26530  ttac  27140  mamufval  27454  sblpnf  27550
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-opab 4080  df-xp 4697
  Copyright terms: Public domain W3C validator