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

Theorem xpeq12d 4864
Description: Equality deduction for Cartesian 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 4858 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  X.  C
)  =  ( B  X.  D ) )
41, 2, 3syl2anc 673 1  |-  ( ph  ->  ( A  X.  C
)  =  ( B  X.  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1452    X. cxp 4837
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-opab 4455  df-xp 4845
This theorem is referenced by:  sqxpeqd  4865  opeliunxp  4891  mpt2mptsx  6875  dmmpt2ssx  6877  fmpt2x  6878  ovmptss  6896  fparlem3  6917  fparlem4  6918  erssxp  7404  marypha2lem2  7968  ackbij1lem8  8675  r1om  8692  fictb  8693  axcc2lem  8884  axcc2  8885  axdc4lem  8903  fsum2dlem  13908  fsumcom2  13912  ackbijnn  13963  fprod2dlem  14111  fprodcom2  14115  homaval  16004  xpcval  16140  xpchom  16143  xpchom2  16149  1stfval  16154  2ndfval  16157  xpcpropd  16171  evlfval  16180  isga  17023  symgval  17098  gsumcom2  17685  gsumxp  17686  ablfaclem3  17798  psrval  18663  mamufval  19487  mamudm  19490  mvmulfval  19644  mavmuldm  19652  mavmul0g  19655  txbas  20659  ptbasfi  20673  txindis  20726  tmsxps  21629  metustexhalf  21649  is2wlkonot  25670  is2spthonot  25671  2wlksot  25674  2spthsot  25675  2wlkonot3v  25682  2spthonot3v  25683  aciunf1lem  28339  esum2dlem  28987  cvmliftlem15  30093  mexval  30212  mpstval  30245  mclsval  30273  mclsax  30279  mclsppslem  30293  filnetlem4  31108  poimirlem26  32030  poimirlem28  32032  heiborlem3  32209  dvhfset  34719  dvhset  34720  dibffval  34779  dibfval  34780  hdmap1fval  35436  opeliun2xp  40622  dmmpt2ssx2  40626
  Copyright terms: Public domain W3C validator