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

Theorem 3eqtr3g 2338
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 2329 . 2  |-  ( ph  ->  C  =  B )
4 3eqtr3g.3 . 2  |-  B  =  D
53, 4syl6eq 2331 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623
This theorem is referenced by:  csbnest1g  3133  xpid11  4900  cores2  5185  funcoeqres  5504  fvunsn  5712  caovmo  6057  dftpos2  6251  tfrlem16  6409  oev2  6522  domss2  7020  enp1ilem  7092  fipreima  7161  dfac5lem3  7752  fpwwe2lem13  8264  canthwelem  8272  canthp1lem2  8275  reclem3pr  8673  mulcmpblnrlem  8695  1idsr  8720  mulgt0sr  8727  mul02lem2  8989  ine0  9215  s1nz  11445  lo1eq  12042  rlimeq  12043  sumeq2ii  12166  fsumf1o  12196  sumss  12197  fsumss  12198  fsumadd  12211  fsumcom2  12237  fsum0diag2  12245  fsummulc2  12246  fsumrelem  12265  isumshft  12298  mertenslem1  12340  bitsinvp1  12640  4sqlem10  12994  setsnid  13188  topnpropd  13341  xpsff1o  13470  homfeqbas  13599  comfffval2  13604  comfeq  13609  oppchomfpropd  13629  isssc  13697  funcpropd  13774  hofpropd  14041  eqglact  14668  lsmmod2  14985  vrgpinv  15078  frgpnabllem1  15161  frgpnabllem2  15162  gsum2d  15223  dprddisj2  15274  ablfac1eulem  15307  rngpropd  15372  crngpropd  15373  mulgass3  15419  rngidpropd  15477  invrpropd  15480  isrhm2d  15506  subrgpropd  15579  rhmpropd  15580  lss0v  15773  lidlrsppropd  15982  ressmpladd  16201  ressmplmul  16202  ressmplvsca  16203  resstopn  16916  lecldbas  16949  ptbasfi  17276  txhaus  17341  divstgplem  17803  imasdsf1olem  17937  reconnlem1  18331  voliunlem1  18907  ismbf3d  19009  i1fima  19033  i1fd  19036  itgfsum  19181  dvmptc  19307  dvmptfsum  19322  dvfsumle  19368  dvfsumlem2  19374  itgsubst  19396  atantayl2  20234  chtdif  20396  ppidif  20401  pythi  21428  hvsubeq0i  21642  hvaddcani  21644  cmcmlem  22170  pj11i  22290  hosubeq0i  22406  riesz3i  22642  pjclem1  22775  pjclem3  22777  st0  22829  chirredi  22974  mdsymi  22991  ballotlemgun  23083  difeq  23128  esumpfinvallem  23442  cvmliftmolem1  23812  cvmlift3lem6  23855  fsumprd  25329  fprodadd  25352  fprodneg  25378  fprodsub  25379  trnij  25615  addcanri  25666  isfne  26268  isfne4  26269  isfne4b  26270  isref  26279  eldioph2  26841  cdlemg47  30925  ltrnco4  30928
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276
  Copyright terms: Public domain W3C validator