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

Theorem xpeq12d 4894
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 4888 . 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 1652    X. cxp 4867
This theorem is referenced by:  opeliunxp  4920  xpcoid  5406  mpt2mptsx  6405  dmmpt2ssx  6407  fmpt2x  6408  ovmptss  6419  fparlem3  6439  fparlem4  6440  erssxp  6919  marypha2lem2  7432  hartogslem1  7500  ackbij1lem8  8096  r1om  8113  fictb  8114  isfin6  8169  axcc2lem  8305  axcc2  8306  axdc4lem  8324  fpwwe2cbv  8494  fpwwe2lem2  8496  fpwwe2lem3  8497  fpwwe2lem8  8501  fpwwe2lem12  8505  fpwwe2lem13  8506  fpwwe2  8507  fpwwecbv  8508  fpwwelem  8509  canthwelem  8514  canthwe  8515  pwfseqlem4  8526  fsum2dlem  12542  fsumcom2  12546  ackbijnn  12595  prdsval  13666  imasval  13725  imasaddfnlem  13741  comfffval  13912  comfeq  13920  oppcval  13927  sscfn1  14005  sscfn2  14006  isssc  14008  ssceq  14014  reschomf  14019  isfunc  14049  idfuval  14061  funcres  14081  funcpropd  14085  fucval  14143  fucpropd  14162  homafval  14172  homaval  14174  setcval  14220  catcval  14239  xpcval  14262  xpchom  14265  xpchom2  14271  1stfval  14276  2ndfval  14279  xpcpropd  14293  evlfval  14302  hofval  14337  hofpropd  14352  istsr  14637  cnvtsr  14642  isdir  14665  tsrdir  14671  frmdval  14784  isga  15056  symgval  15082  gsumcom2  15537  gsumxp  15538  ablfaclem3  15633  psrval  16417  opsrval  16523  txbas  17587  ptbasfi  17601  txindis  17654  ustval  18220  trust  18247  utop2nei  18268  utop3cls  18269  utopreg  18270  ussval  18277  ressuss  18281  tususs  18288  fmucnd  18310  cfilufg  18311  trcfilu  18312  neipcfilu  18314  ispsmet  18323  prdsdsf  18385  prdsxmet  18387  ressprdsds  18389  xpsdsfn2  18396  xpsxmetlem  18397  xpsmet  18400  isxms  18465  isms  18467  xmspropd  18491  mspropd  18492  setsxms  18497  setsms  18498  imasf1oxms  18507  imasf1oms  18508  ressxms  18543  ressms  18544  prdsxmslem2  18547  tmsxps  18554  metuvalOLD  18567  metuval  18568  metustexhalfOLD  18581  metustexhalf  18582  nmpropd2  18630  ngppropd  18666  tngngp2  18681  pi1addf  19060  pi1addval  19061  iscms  19286  cmspropd  19290  cmsss  19291  cmetcusp  19296  minveclem3a  19316  dvlip2  19867  dchrval  21006  isgrp2d  21811  isgrpda  21873  efghgrp  21949  isrngo  21954  isrngod  21955  rngosn3  22002  isdivrngo  22007  issh  22698  sibfof  24642  sitgclcn  24646  sitgclre  24647  cvmliftlem15  24973  fprod2dlem  25293  fprodcom2  25297  brcgr  25787  funtransport  25913  fvtransport  25914  filnetlem4  26347  prdsbnd2  26441  cnpwstotbnd  26443  heiborlem3  26459  aomclem8  27074  mamufval  27358  matval  27380  is2wlkonot  28204  is2spthonot  28205  2wlksot  28208  2spthsot  28209  2wlkonot3v  28216  2spthonot3v  28217  ldualset  29762  dvhfset  31717  dvhset  31718  dibffval  31777  dibfval  31778  hdmap1fval  32434
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-opab 4259  df-xp 4875
  Copyright terms: Public domain W3C validator