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

Theorem xpeq12d 4862
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 4856 . 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 4835
This theorem is referenced by:  opeliunxp  4888  xpcoid  5374  mpt2mptsx  6373  dmmpt2ssx  6375  fmpt2x  6376  ovmptss  6387  fparlem3  6407  fparlem4  6408  erssxp  6887  marypha2lem2  7399  hartogslem1  7467  ackbij1lem8  8063  r1om  8080  fictb  8081  isfin6  8136  axcc2lem  8272  axcc2  8273  axdc4lem  8291  fpwwe2cbv  8461  fpwwe2lem2  8463  fpwwe2lem3  8464  fpwwe2lem8  8468  fpwwe2lem12  8472  fpwwe2lem13  8473  fpwwe2  8474  fpwwecbv  8475  fpwwelem  8476  canthwelem  8481  canthwe  8482  pwfseqlem4  8493  fsum2dlem  12509  fsumcom2  12513  ackbijnn  12562  prdsval  13633  imasval  13692  imasaddfnlem  13708  comfffval  13879  comfeq  13887  oppcval  13894  sscfn1  13972  sscfn2  13973  isssc  13975  ssceq  13981  reschomf  13986  isfunc  14016  idfuval  14028  funcres  14048  funcpropd  14052  fucval  14110  fucpropd  14129  homafval  14139  homaval  14141  setcval  14187  catcval  14206  xpcval  14229  xpchom  14232  xpchom2  14238  1stfval  14243  2ndfval  14246  xpcpropd  14260  evlfval  14269  hofval  14304  hofpropd  14319  istsr  14604  cnvtsr  14609  isdir  14632  tsrdir  14638  frmdval  14751  isga  15023  symgval  15049  gsumcom2  15504  gsumxp  15505  ablfaclem3  15600  psrval  16384  opsrval  16490  txbas  17552  ptbasfi  17566  txindis  17619  ustval  18185  trust  18212  utop2nei  18233  utop3cls  18234  utopreg  18235  ussval  18242  ressuss  18246  tususs  18253  fmucnd  18275  cfilufg  18276  trcfilu  18277  neipcfilu  18279  ispsmet  18288  prdsdsf  18350  prdsxmet  18352  ressprdsds  18354  xpsdsfn2  18361  xpsxmetlem  18362  xpsmet  18365  isxms  18430  isms  18432  xmspropd  18456  mspropd  18457  setsxms  18462  setsms  18463  imasf1oxms  18472  imasf1oms  18473  ressxms  18508  ressms  18509  prdsxmslem2  18512  tmsxps  18519  metuvalOLD  18532  metuval  18533  metustexhalfOLD  18546  metustexhalf  18547  nmpropd2  18595  ngppropd  18631  tngngp2  18646  pi1addf  19025  pi1addval  19026  iscms  19251  cmspropd  19255  cmsss  19256  cmetcusp  19261  minveclem3a  19281  dvlip2  19832  dchrval  20971  isgrp2d  21776  isgrpda  21838  efghgrp  21914  isrngo  21919  isrngod  21920  rngosn3  21967  isdivrngo  21972  issh  22663  sibfof  24607  sitgclcn  24611  sitgclre  24612  cvmliftlem15  24938  fprod2dlem  25257  fprodcom2  25261  brcgr  25743  funtransport  25869  fvtransport  25870  filnetlem4  26300  prdsbnd2  26394  cnpwstotbnd  26396  heiborlem3  26412  aomclem8  27027  mamufval  27311  matval  27333  is2wlkonot  28060  is2spthonot  28061  2wlksot  28064  2spthsot  28065  2wlkonot3v  28072  2spthonot3v  28073  ldualset  29608  dvhfset  31563  dvhset  31564  dibffval  31623  dibfval  31624  hdmap1fval  32280
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
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 2391  df-cleq 2397  df-clel 2400  df-opab 4227  df-xp 4843
  Copyright terms: Public domain W3C validator