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

Theorem xpeq12d 4903
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 4897 . 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 4876
This theorem is referenced by:  opeliunxp  4929  xpcoid  5415  mpt2mptsx  6414  dmmpt2ssx  6416  fmpt2x  6417  ovmptss  6428  fparlem3  6448  fparlem4  6449  erssxp  6928  marypha2lem2  7441  hartogslem1  7511  ackbij1lem8  8107  r1om  8124  fictb  8125  isfin6  8180  axcc2lem  8316  axcc2  8317  axdc4lem  8335  fpwwe2cbv  8505  fpwwe2lem2  8507  fpwwe2lem3  8508  fpwwe2lem8  8512  fpwwe2lem12  8516  fpwwe2lem13  8517  fpwwe2  8518  fpwwecbv  8519  fpwwelem  8520  canthwelem  8525  canthwe  8526  pwfseqlem4  8537  fsum2dlem  12554  fsumcom2  12558  ackbijnn  12607  prdsval  13678  imasval  13737  imasaddfnlem  13753  comfffval  13924  comfeq  13932  oppcval  13939  sscfn1  14017  sscfn2  14018  isssc  14020  ssceq  14026  reschomf  14031  isfunc  14061  idfuval  14073  funcres  14093  funcpropd  14097  fucval  14155  fucpropd  14174  homafval  14184  homaval  14186  setcval  14232  catcval  14251  xpcval  14274  xpchom  14277  xpchom2  14283  1stfval  14288  2ndfval  14291  xpcpropd  14305  evlfval  14314  hofval  14349  hofpropd  14364  istsr  14649  cnvtsr  14654  isdir  14677  tsrdir  14683  frmdval  14796  isga  15068  symgval  15094  gsumcom2  15549  gsumxp  15550  ablfaclem3  15645  psrval  16429  opsrval  16535  txbas  17599  ptbasfi  17613  txindis  17666  ustval  18232  trust  18259  utop2nei  18280  utop3cls  18281  utopreg  18282  ussval  18289  ressuss  18293  tususs  18300  fmucnd  18322  cfilufg  18323  trcfilu  18324  neipcfilu  18326  ispsmet  18335  prdsdsf  18397  prdsxmet  18399  ressprdsds  18401  xpsdsfn2  18408  xpsxmetlem  18409  xpsmet  18412  isxms  18477  isms  18479  xmspropd  18503  mspropd  18504  setsxms  18509  setsms  18510  imasf1oxms  18519  imasf1oms  18520  ressxms  18555  ressms  18556  prdsxmslem2  18559  tmsxps  18566  metuvalOLD  18579  metuval  18580  metustexhalfOLD  18593  metustexhalf  18594  nmpropd2  18642  ngppropd  18678  tngngp2  18693  pi1addf  19072  pi1addval  19073  iscms  19298  cmspropd  19302  cmsss  19303  cmetcusp  19308  minveclem3a  19328  dvlip2  19879  dchrval  21018  isgrp2d  21823  isgrpda  21885  efghgrp  21961  isrngo  21966  isrngod  21967  rngosn3  22014  isdivrngo  22019  issh  22710  sibfof  24654  sitgclcn  24658  sitgclre  24659  cvmliftlem15  24985  fprod2dlem  25304  fprodcom2  25308  brcgr  25839  funtransport  25965  fvtransport  25966  filnetlem4  26410  prdsbnd2  26504  cnpwstotbnd  26506  heiborlem3  26522  aomclem8  27136  mamufval  27420  matval  27442  is2wlkonot  28330  is2spthonot  28331  2wlksot  28334  2spthsot  28335  2wlkonot3v  28342  2spthonot3v  28343  ldualset  29923  dvhfset  31878  dvhset  31879  dibffval  31938  dibfval  31939  hdmap1fval  32595
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 2417
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 2423  df-cleq 2429  df-clel 2432  df-opab 4267  df-xp 4884
  Copyright terms: Public domain W3C validator