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

Theorem xpeq12d 4844
Description: Equality deduction for cross product. (Contributed by NM, 8-Dec-2013.)
Hypotheses
Ref Expression
xpeq1d.1  |-  ( ph  ->  A  =  B )
xpeq12d.2  |-  ( ph  ->  C  =  D )
Assertion
Ref Expression
xpeq12d  |-  ( ph  ->  ( A  X.  C
)  =  ( B  X.  D ) )

Proof of Theorem xpeq12d
StepHypRef Expression
1 xpeq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 xpeq12d.2 . 2  |-  ( ph  ->  C  =  D )
3 xpeq12 4838 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  X.  C
)  =  ( B  X.  D ) )
41, 2, 3syl2anc 643 1  |-  ( ph  ->  ( A  X.  C
)  =  ( B  X.  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    X. cxp 4817
This theorem is referenced by:  opeliunxp  4870  xpcoid  5356  mpt2mptsx  6354  dmmpt2ssx  6356  fmpt2x  6357  ovmptss  6368  fparlem3  6388  fparlem4  6389  erssxp  6865  marypha2lem2  7377  hartogslem1  7445  ackbij1lem8  8041  r1om  8058  fictb  8059  isfin6  8114  axcc2lem  8250  axcc2  8251  axdc4lem  8269  fpwwe2cbv  8439  fpwwe2lem2  8441  fpwwe2lem3  8442  fpwwe2lem8  8446  fpwwe2lem12  8450  fpwwe2lem13  8451  fpwwe2  8452  fpwwecbv  8453  fpwwelem  8454  canthwelem  8459  canthwe  8460  pwfseqlem4  8471  fsum2dlem  12482  fsumcom2  12486  ackbijnn  12535  prdsval  13606  imasval  13665  imasaddfnlem  13681  comfffval  13852  comfeq  13860  oppcval  13867  sscfn1  13945  sscfn2  13946  isssc  13948  ssceq  13954  reschomf  13959  isfunc  13989  idfuval  14001  funcres  14021  funcpropd  14025  fucval  14083  fucpropd  14102  homafval  14112  homaval  14114  setcval  14160  catcval  14179  xpcval  14202  xpchom  14205  xpchom2  14211  1stfval  14216  2ndfval  14219  xpcpropd  14233  evlfval  14242  hofval  14277  hofpropd  14292  istsr  14577  cnvtsr  14582  isdir  14605  tsrdir  14611  frmdval  14724  isga  14996  symgval  15022  gsumcom2  15477  gsumxp  15478  ablfaclem3  15573  psrval  16357  opsrval  16463  txbas  17521  ptbasfi  17535  txindis  17588  ustval  18154  trust  18181  utop2nei  18202  utop3cls  18203  utopreg  18204  ussval  18211  ressuss  18215  tususs  18222  fmucnd  18244  cfilufg  18245  trcfilu  18246  neipcfilu  18248  prdsdsf  18306  prdsxmet  18308  ressprdsds  18310  xpsdsfn2  18317  xpsxmetlem  18318  xpsmet  18321  isxms  18368  isms  18370  xmspropd  18394  mspropd  18395  setsxms  18400  setsms  18401  imasf1oxms  18410  imasf1oms  18411  ressxms  18446  ressms  18447  prdsxmslem2  18450  tmsxps  18457  metuval  18470  metustexhalf  18477  nmpropd2  18514  ngppropd  18550  tngngp2  18565  pi1addf  18944  pi1addval  18945  iscms  19168  cmspropd  19172  cmsss  19173  minveclem3a  19196  dvlip2  19747  dchrval  20886  isgrp2d  21672  isgrpda  21734  efghgrp  21810  isrngo  21815  isrngod  21816  rngosn3  21863  isdivrngo  21868  issh  22559  cvmliftlem15  24765  brcgr  25554  funtransport  25680  fvtransport  25681  filnetlem4  26102  prdsbnd2  26196  cnpwstotbnd  26198  heiborlem3  26214  aomclem8  26829  mamufval  27113  matval  27135  ldualset  29241  dvhfset  31196  dvhset  31197  dibffval  31256  dibfval  31257  hdmap1fval  31913
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2375  df-cleq 2381  df-clel 2384  df-opab 4209  df-xp 4825
  Copyright terms: Public domain W3C validator