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

Theorem xpeq12d 4716
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 4710 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  X.  C
)  =  ( B  X.  D ) )
41, 2, 3syl2anc 642 1  |-  ( ph  ->  ( A  X.  C
)  =  ( B  X.  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1625    X. cxp 4689
This theorem is referenced by:  opeliunxp  4742  mpt2mptsx  6189  dmmpt2ssx  6191  fmpt2x  6192  ovmptss  6202  fparlem3  6222  fparlem4  6223  erssxp  6685  marypha2lem2  7191  hartogslem1  7259  ackbij1lem8  7855  r1om  7872  fictb  7873  isfin6  7928  axcc2lem  8064  axcc2  8065  axdc4lem  8083  fpwwe2cbv  8254  fpwwe2lem2  8256  fpwwe2lem3  8257  fpwwe2lem8  8261  fpwwe2lem12  8265  fpwwe2lem13  8266  fpwwe2  8267  fpwwecbv  8268  fpwwelem  8269  canthwelem  8274  canthwe  8275  pwfseqlem4  8286  fsum2dlem  12235  fsumcom2  12239  ackbijnn  12288  prdsval  13357  imasval  13416  imasaddfnlem  13432  comfffval  13603  comfeq  13611  oppcval  13618  sscfn1  13696  sscfn2  13697  isssc  13699  ssceq  13705  reschomf  13710  isfunc  13740  idfuval  13752  funcres  13772  funcpropd  13776  fucval  13834  fucpropd  13853  homafval  13863  homaval  13865  setcval  13911  catcval  13930  xpcval  13953  xpchom  13956  xpchom2  13962  1stfval  13967  2ndfval  13970  xpcpropd  13984  evlfval  13993  hofval  14028  hofpropd  14043  istsr  14328  cnvtsr  14333  isdir  14356  tsrdir  14362  frmdval  14475  isga  14747  symgval  14773  gsumcom2  15228  gsumxp  15229  ablfaclem3  15324  psrval  16112  opsrval  16218  txbas  17264  ptbasfi  17278  txindis  17330  prdsdsf  17933  prdsxmet  17935  ressprdsds  17937  xpsdsfn2  17944  xpsxmetlem  17945  xpsmet  17948  isxms  17995  isms  17997  xmspropd  18021  mspropd  18022  setsxms  18027  setsms  18028  imasf1oxms  18037  imasf1oms  18038  ressxms  18073  ressms  18074  prdsxmslem2  18077  tmsxps  18084  nmpropd2  18119  ngppropd  18155  tngngp2  18170  pi1addf  18547  pi1addval  18548  iscms  18769  cmspropd  18773  cmsss  18774  minveclem3a  18793  dvlip2  19344  dchrval  20475  isgrp2d  20904  isgrpda  20966  efghgrp  21042  isrngo  21047  isrngod  21048  rngosn3  21095  isdivrngo  21100  issh  21789  dya2iocrrnval  23584  cvmliftlem15  23831  brcgr  24530  funtransport  24656  fvtransport  24657  domrancur1b  25211  tcnvec  25701  isalg  25732  dualalg  25793  issubcat  25856  setiscat  25990  nds  26161  filnetlem4  26341  prdsbnd2  26530  cnpwstotbnd  26532  heiborlem3  26548  aomclem8  27170  mamufval  27454  matval  27476  ldualset  29388  dvhfset  31343  dvhset  31344  dibffval  31403  dibfval  31404  hdmap1fval  32060
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