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

Theorem 3eqtr3g 2351
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 2342 . 2  |-  ( ph  ->  C  =  B )
4 3eqtr3g.3 . 2  |-  B  =  D
53, 4syl6eq 2344 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632
This theorem is referenced by:  csbnest1g  3146  xpid11  4916  cores2  5201  funcoeqres  5520  fvunsn  5728  caovmo  6073  dftpos2  6267  tfrlem16  6425  oev2  6538  domss2  7036  enp1ilem  7108  fipreima  7177  dfac5lem3  7768  fpwwe2lem13  8280  canthwelem  8288  canthp1lem2  8291  reclem3pr  8689  mulcmpblnrlem  8711  1idsr  8736  mulgt0sr  8743  mul02lem2  9005  ine0  9231  s1nz  11461  lo1eq  12058  rlimeq  12059  sumeq2ii  12182  fsumf1o  12212  sumss  12213  fsumss  12214  fsumadd  12227  fsumcom2  12253  fsum0diag2  12261  fsummulc2  12262  fsumrelem  12281  isumshft  12314  mertenslem1  12356  bitsinvp1  12656  4sqlem10  13010  setsnid  13204  topnpropd  13357  xpsff1o  13486  homfeqbas  13615  comfffval2  13620  comfeq  13625  oppchomfpropd  13645  isssc  13713  funcpropd  13790  hofpropd  14057  eqglact  14684  lsmmod2  15001  vrgpinv  15094  frgpnabllem1  15177  frgpnabllem2  15178  gsum2d  15239  dprddisj2  15290  ablfac1eulem  15323  rngpropd  15388  crngpropd  15389  mulgass3  15435  rngidpropd  15493  invrpropd  15496  isrhm2d  15522  subrgpropd  15595  rhmpropd  15596  lss0v  15789  lidlrsppropd  15998  ressmpladd  16217  ressmplmul  16218  ressmplvsca  16219  resstopn  16932  lecldbas  16965  ptbasfi  17292  txhaus  17357  divstgplem  17819  imasdsf1olem  17953  reconnlem1  18347  voliunlem1  18923  ismbf3d  19025  i1fima  19049  i1fd  19052  itgfsum  19197  dvmptc  19323  dvmptfsum  19338  dvfsumle  19384  dvfsumlem2  19390  itgsubst  19412  atantayl2  20250  chtdif  20412  ppidif  20417  pythi  21444  hvsubeq0i  21658  hvaddcani  21660  cmcmlem  22186  pj11i  22306  hosubeq0i  22422  riesz3i  22658  pjclem1  22791  pjclem3  22793  st0  22845  chirredi  22990  mdsymi  23007  ballotlemgun  23099  difeq  23144  esumpfinvallem  23457  cvmliftmolem1  23827  cvmlift3lem6  23870  cprodeq2ii  24135  fprodf1o  24172  fsumprd  25432  fprodadd  25455  fprodneg  25481  fprodsub  25482  trnij  25718  addcanri  25769  isfne  26371  isfne4  26372  isfne4b  26373  isref  26382  eldioph2  26944  cdlemg47  31547  ltrnco4  31550
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-cleq 2289
  Copyright terms: Public domain W3C validator