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

Theorem 3eqtr3g 2493
Description: A chained equality inference, useful for converting from definitions. (Contributed by NM, 15-Nov-1994.)
Hypotheses
Ref Expression
3eqtr3g.1  |-  ( ph  ->  A  =  B )
3eqtr3g.2  |-  A  =  C
3eqtr3g.3  |-  B  =  D
Assertion
Ref Expression
3eqtr3g  |-  ( ph  ->  C  =  D )

Proof of Theorem 3eqtr3g
StepHypRef Expression
1 3eqtr3g.2 . . 3  |-  A  =  C
2 3eqtr3g.1 . . 3  |-  ( ph  ->  A  =  B )
31, 2syl5eqr 2484 . 2  |-  ( ph  ->  C  =  B )
4 3eqtr3g.3 . 2  |-  B  =  D
53, 4syl6eq 2486 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-ex 1587  df-cleq 2431
This theorem is referenced by:  csbnest1g  3692  tppreqb  4009  xpid11  5056  cores2  5345  funcoeqres  5666  fvunsn  5905  caovmo  6295  dftpos2  6757  tfrlem16  6844  oev2  6955  domss2  7462  enp1ilem  7538  fipreima  7609  dfac5lem3  8287  fpwwe2lem13  8801  canthwelem  8809  canthp1lem2  8812  reclem3pr  9210  mulcmpblnrlem  9232  1idsr  9257  mulgt0sr  9264  mul02lem2  9538  ine0  9772  s1nz  12289  lo1eq  13038  rlimeq  13039  sumeq2ii  13162  fsumf1o  13192  sumss  13193  fsumss  13194  fsumadd  13207  fsumcom2  13233  fsum0diag2  13242  fsummulc2  13243  fsumrelem  13262  isumshft  13294  mertenslem1  13336  bitsinv1  13630  bitsinvp1  13637  4sqlem10  14000  setsnid  14208  topnpropd  14367  xpsff1o  14498  homfeqbas  14627  comfffval2  14632  comfeq  14637  oppchomfpropd  14657  isssc  14725  funcpropd  14802  hofpropd  15069  eqglact  15723  lsmmod2  16164  vrgpinv  16257  frgpnabllem1  16342  frgpnabllem2  16343  gsum2dlem2  16450  gsum2dOLD  16452  dprddisj2  16525  dprddisj2OLD  16526  ablfac1eulem  16561  rngpropd  16664  crngpropd  16665  mulgass3  16717  rngidpropd  16775  invrpropd  16778  isrhm2d  16804  subrgpropd  16877  rhmpropd  16878  lss0v  17074  lidlrsppropd  17289  ressmpladd  17513  ressmplmul  17514  ressmplvsca  17515  resstopn  18765  lecldbas  18798  ptbasfi  19129  txhaus  19195  divstgplem  19666  tuslem  19817  imasdsf1olem  19923  metustsymOLD  20111  metustsym  20112  reconnlem1  20378  voliunlem1  21006  ismbf3d  21107  i1fima  21131  i1fd  21134  itgfsum  21279  dvmptc  21407  dvmptfsum  21422  dvfsumle  21468  dvfsumlem2  21474  itgsubst  21496  atantayl2  22308  chtdif  22471  ppidif  22476  pythi  24201  hvsubeq0i  24416  hvaddcani  24418  cmcmlem  24945  pj11i  25065  hosubeq0i  25181  riesz3i  25417  pjclem1  25550  pjclem3  25552  st0  25604  chirredi  25749  mdsymi  25766  difeq  25850  subrgchr  26213  esumpfinvallem  26475  ballotlemgun  26859  cvmliftmolem1  27122  cvmlift3lem6  27165  prodeq2ii  27377  fprodf1o  27410  prodss  27411  fprodss  27412  fprodmul  27422  fproddiv  27423  fprodefsum  27436  fprodcom2  27446  ptrest  28378  mblfinlem2  28382  voliunnfl  28388  isfne  28493  isfne4  28494  isfne4b  28495  isref  28504  eldioph2  29053  rnfdmpr  30102  bj-disjdif  32293  bj-1uplth  32347  bj-2uplth  32361  cdlemg47  34220  ltrnco4  34223
  Copyright terms: Public domain W3C validator