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

Theorem 3eqtr3g 2490
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 2481 . 2  |-  ( ph  ->  C  =  B )
4 3eqtr3g.3 . 2  |-  B  =  D
53, 4syl6eq 2483 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652
This theorem is referenced by:  csbnest1g  3295  tppreqb  3931  xpid11  5083  cores2  5374  funcoeqres  5698  fvunsn  5917  caovmo  6276  dftpos2  6488  tfrlem16  6646  oev2  6759  domss2  7258  enp1ilem  7334  fipreima  7404  dfac5lem3  7996  fpwwe2lem13  8507  canthwelem  8515  canthp1lem2  8518  reclem3pr  8916  mulcmpblnrlem  8938  1idsr  8963  mulgt0sr  8970  mul02lem2  9233  ine0  9459  s1nz  11749  lo1eq  12352  rlimeq  12353  sumeq2ii  12477  fsumf1o  12507  sumss  12508  fsumss  12509  fsumadd  12522  fsumcom2  12548  fsum0diag2  12556  fsummulc2  12557  fsumrelem  12576  isumshft  12609  mertenslem1  12651  bitsinv1  12944  bitsinvp1  12951  4sqlem10  13305  setsnid  13499  topnpropd  13654  xpsff1o  13783  homfeqbas  13912  comfffval2  13917  comfeq  13922  oppchomfpropd  13942  isssc  14010  funcpropd  14087  hofpropd  14354  eqglact  14981  lsmmod2  15298  vrgpinv  15391  frgpnabllem1  15474  frgpnabllem2  15475  gsum2d  15536  dprddisj2  15587  ablfac1eulem  15620  rngpropd  15685  crngpropd  15686  mulgass3  15732  rngidpropd  15790  invrpropd  15793  isrhm2d  15819  subrgpropd  15892  rhmpropd  15893  lss0v  16082  lidlrsppropd  16291  ressmpladd  16510  ressmplmul  16511  ressmplvsca  16512  resstopn  17240  lecldbas  17273  ptbasfi  17603  txhaus  17669  divstgplem  18140  tuslem  18287  imasdsf1olem  18393  metustsymOLD  18581  metustsym  18582  reconnlem1  18847  voliunlem1  19434  ismbf3d  19536  i1fima  19560  i1fd  19563  itgfsum  19708  dvmptc  19834  dvmptfsum  19849  dvfsumle  19895  dvfsumlem2  19901  itgsubst  19923  atantayl2  20768  chtdif  20931  ppidif  20936  pythi  22341  hvsubeq0i  22555  hvaddcani  22557  cmcmlem  23083  pj11i  23203  hosubeq0i  23319  riesz3i  23555  pjclem1  23688  pjclem3  23690  st0  23742  chirredi  23887  mdsymi  23904  difeq  23988  subrgchr  24220  esumpfinvallem  24454  ballotlemgun  24772  cvmliftmolem1  24958  cvmlift3lem6  25001  prodeq2ii  25229  fprodf1o  25262  prodss  25263  fprodss  25264  fprodmul  25274  fproddiv  25275  fprodefsum  25288  fprodcom2  25298  mblfinlem  26207  voliunnfl  26213  isfne  26302  isfne4  26303  isfne4b  26304  isref  26313  eldioph2  26774  rnfdmpr  28033  cdlemg47  31434  ltrnco4  31437
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-cleq 2428
  Copyright terms: Public domain W3C validator