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

Theorem 3eqtr3g 2531
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 2522 . 2  |-  ( ph  ->  C  =  B )
4 3eqtr3g.3 . 2  |-  B  =  D
53, 4syl6eq 2524 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-cleq 2459
This theorem is referenced by:  csbnest1g  3845  tppreqb  4168  xpid11  5223  cores2  5519  funcoeqres  5845  fvunsn  6092  caovmo  6495  dftpos2  6972  fvmpt2curryd  7000  tfrlem16  7062  oev2  7173  domss2  7676  enp1ilem  7753  fipreima  7825  dfac5lem3  8505  fpwwe2lem13  9019  canthwelem  9027  canthp1lem2  9030  reclem3pr  9426  mulcmpblnrlem  9446  1idsr  9474  mulgt0sr  9481  mul02lem2  9755  ine0  9991  s1nz  12580  lo1eq  13353  rlimeq  13354  sumeq2ii  13477  fsumf1o  13507  sumss  13508  fsumss  13509  fsumadd  13523  fsumcom2  13551  fsum0diag2  13560  fsummulc2  13561  fsumrelem  13583  isumshft  13613  mertenslem1  13655  bitsinv1  13950  bitsinvp1  13957  4sqlem10  14323  setsnid  14531  topnpropd  14691  xpsff1o  14822  homfeqbas  14951  comfffval2  14956  comfeq  14961  oppchomfpropd  14981  isssc  15049  funcpropd  15126  hofpropd  15393  eqglact  16054  lsmmod2  16497  vrgpinv  16590  frgpnabllem1  16677  frgpnabllem2  16678  gsum2dlem2  16798  gsum2dOLD  16800  dprddisj2  16886  dprddisj2OLD  16887  ablfac1eulem  16922  rngpropd  17026  crngpropd  17027  mulgass3  17082  rngidpropd  17140  invrpropd  17143  isrhm2d  17173  subrgpropd  17258  rhmpropd  17259  lss0v  17457  lidlrsppropd  17672  ressmpladd  17906  ressmplmul  17907  ressmplvsca  17908  eqcoe1ply1eq  18126  resstopn  19469  lecldbas  19502  ptbasfi  19833  txhaus  19899  divstgplem  20370  tuslem  20521  imasdsf1olem  20627  metustsymOLD  20815  metustsym  20816  reconnlem1  21082  voliunlem1  21711  ismbf3d  21812  i1fima  21836  i1fd  21839  itgfsum  21984  dvmptc  22112  dvmptfsum  22127  dvfsumle  22173  dvfsumlem2  22179  itgsubst  22201  atantayl2  23013  chtdif  23176  ppidif  23181  pythi  25457  hvsubeq0i  25672  hvaddcani  25674  cmcmlem  26201  pj11i  26321  hosubeq0i  26437  riesz3i  26673  pjclem1  26806  pjclem3  26808  st0  26860  chirredi  27005  mdsymi  27022  difeq  27106  subrgchr  27463  esumpfinvallem  27736  ballotlemgun  28119  cvmliftmolem1  28382  cvmlift3lem6  28425  prodeq2ii  28638  fprodf1o  28671  prodss  28672  fprodss  28673  fprodmul  28683  fproddiv  28684  fprodefsum  28697  fprodcom2  28707  ptrest  29641  mblfinlem2  29645  voliunnfl  29651  isfne  29756  isfne4  29757  isfne4b  29758  isref  29767  eldioph2  30315  rnfdmpr  31791  bj-disjdif  33601  bj-1uplth  33655  bj-2uplth  33669  cdlemg47  35541  ltrnco4  35544
  Copyright terms: Public domain W3C validator