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

Theorem 3eqtr3g 2521
Description: A chained equality inference, useful for converting from definitions. (Contributed by NM, 15-Nov-1994.)
Hypotheses
Ref Expression
3eqtr3g.1
3eqtr3g.2
3eqtr3g.3
Assertion
Ref Expression
3eqtr3g

Proof of Theorem 3eqtr3g
StepHypRef Expression
1 3eqtr3g.2 . . 3
2 3eqtr3g.1 . . 3
31, 2syl5eqr 2512 . 2
4 3eqtr3g.3 . 2
53, 4syl6eq 2514 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395
This theorem is referenced by:  csbnest1g  3845  tppreqb  4171  xpid11  5229  cores2  5525  funcoeqres  5851  fvunsn  6103  caovmo  6512  dftpos2  6991  fvmpt2curryd  7019  tfrlem16  7081  oev2  7192  domss2  7696  enp1ilem  7774  fipreima  7846  dfac5lem3  8527  fpwwe2lem13  9041  canthwelem  9049  canthp1lem2  9052  reclem3pr  9448  mulcmpblnrlem  9468  1idsr  9496  mulgt0sr  9503  mul02lem2  9778  ine0  10017  s1nz  12618  lo1eq  13391  rlimeq  13392  sumeq2ii  13515  fsumf1o  13545  sumss  13546  fsumss  13547  fsumadd  13561  fsumcom2  13589  fsum0diag2  13598  fsummulc2  13599  fsumrelem  13621  isumshft  13651  mertenslem1  13693  prodeq2ii  13720  fprodf1o  13753  prodss  13754  fprodss  13755  fprodmul  13765  fproddiv  13766  fprodcom2  13788  fprodefsum  13830  bitsinv1  14092  bitsinvp1  14099  4sqlem10  14465  setsnid  14674  topnpropd  14834  xpsff1o  14965  homfeqbas  15091  comfffval2  15096  comfeq  15101  oppchomfpropd  15121  isssc  15189  funcpropd  15269  hofpropd  15536  eqglact  16252  lsmmod2  16694  vrgpinv  16787  frgpnabllem1  16877  frgpnabllem2  16878  gsum2dlem2  16998  gsum2dOLD  17000  dprddisj2  17087  dprddisj2OLD  17088  ablfac1eulem  17123  ringpropd  17230  crngpropd  17231  mulgass3  17286  rngidpropd  17344  invrpropd  17347  isrhm2d  17377  subrgpropd  17463  rhmpropd  17464  lss0v  17662  lidlrsppropd  17878  ressmpladd  18119  ressmplmul  18120  ressmplvsca  18121  eqcoe1ply1eq  18339  resstopn  19687  lecldbas  19720  isref  20010  ptbasfi  20082  txhaus  20148  qustgplem  20619  tuslem  20770  imasdsf1olem  20876  metustsymOLD  21064  metustsym  21065  reconnlem1  21331  voliunlem1  21960  ismbf3d  22061  i1fima  22085  i1fd  22088  itgfsum  22233  dvmptc  22361  dvmptfsum  22376  dvfsumle  22422  dvfsumlem2  22428  itgsubst  22450  atantayl2  23269  chtdif  23432  ppidif  23437  pythi  25765  hvsubeq0i  25980  hvaddcani  25982  cmcmlem  26509  pj11i  26629  hosubeq0i  26745  riesz3i  26981  pjclem1  27114  pjclem3  27116  st0  27168  chirredi  27313  mdsymi  27330  difeq  27416  subrgchr  27784  locfinref  27844  esumpfinvallem  28080  ballotlemgun  28463  cvmliftmolem1  28726  cvmlift3lem6  28769  msubff1  28916  ptrest  30048  mblfinlem2  30052  voliunnfl  30058  isfne  30157  isfne4  30158  isfne4b  30159  eldioph2  30695  binomcxplemdvbinom  31258  binomcxplemnotnn0  31261  dvmptfprodlem  31741  rnfdmpr  32308  bj-disjdif  34511  bj-1uplth  34565  bj-2uplth  34579  cdlemg47  36462  ltrnco4  36465
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-cleq 2449
  Copyright terms: Public domain W3C validator