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

Theorem xpeq12d 5014
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 5008 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  X.  C
)  =  ( B  X.  D ) )
41, 2, 3syl2anc 661 1  |-  ( ph  ->  ( A  X.  C
)  =  ( B  X.  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1383    X. cxp 4987
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-opab 4496  df-xp 4995
This theorem is referenced by:  sqxpeqd  5015  opeliunxp  5041  mpt2mptsx  6848  dmmpt2ssx  6850  fmpt2x  6851  ovmptss  6866  fparlem3  6887  fparlem4  6888  erssxp  7336  marypha2lem2  7898  ackbij1lem8  8610  r1om  8627  fictb  8628  axcc2lem  8819  axcc2  8820  axdc4lem  8838  fsum2dlem  13567  fsumcom2  13571  ackbijnn  13622  fprod2dlem  13766  fprodcom2  13770  homaval  15337  xpcval  15425  xpchom  15428  xpchom2  15434  1stfval  15439  2ndfval  15442  xpcpropd  15456  evlfval  15465  isga  16308  symgval  16383  gsumcom2  16982  gsumxp  16983  gsumxpOLD  16985  ablfaclem3  17117  psrval  17990  mamufval  18865  mamudm  18868  mvmulfval  19022  mavmuldm  19030  mavmul0g  19033  txbas  20046  ptbasfi  20060  txindis  20113  tmsxps  21017  metuvalOLD  21030  metustexhalfOLD  21044  metustexhalf  21045  is2wlkonot  24841  is2spthonot  24842  2wlksot  24845  2spthsot  24846  2wlkonot3v  24853  2spthonot3v  24854  cvmliftlem15  28721  mexval  28840  mpstval  28873  mclsval  28901  mclsax  28907  mclsppslem  28921  filnetlem4  30175  heiborlem3  30285  opeliun2xp  32790  dmmpt2ssx2  32794  dvhfset  36682  dvhset  36683  dibffval  36742  dibfval  36743  hdmap1fval  37399
  Copyright terms: Public domain W3C validator