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

Theorem 3eqtr2rd 2335
Description: A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.)
Hypotheses
Ref Expression
3eqtr2d.1  |-  ( ph  ->  A  =  B )
3eqtr2d.2  |-  ( ph  ->  C  =  B )
3eqtr2d.3  |-  ( ph  ->  C  =  D )
Assertion
Ref Expression
3eqtr2rd  |-  ( ph  ->  D  =  A )

Proof of Theorem 3eqtr2rd
StepHypRef Expression
1 3eqtr2d.1 . . 3  |-  ( ph  ->  A  =  B )
2 3eqtr2d.2 . . 3  |-  ( ph  ->  C  =  B )
31, 2eqtr4d 2331 . 2  |-  ( ph  ->  A  =  C )
4 3eqtr2d.3 . 2  |-  ( ph  ->  C  =  D )
53, 4eqtr2d 2329 1  |-  ( ph  ->  D  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632
This theorem is referenced by:  nneob  6666  faclbnd2  11320  cats1un  11492  cjmulval  11646  fsumsplit  12228  fzosump1  12233  bcxmas  12310  trireciplem  12336  geo2sum  12345  geo2lim  12347  geoisum1c  12352  mertenslem1  12356  eftlub  12405  tanadd  12463  addsin  12466  subsin  12467  subcos  12471  sadadd2lem2  12657  qredeu  12802  zsqrelqelz  12845  4sqlem15  13022  resssetc  13940  resscatc  13953  curfcl  14022  conjghm  14729  gasubg  14772  dfod2  14893  efginvrel2  15052  efgcpbllemb  15080  odadd2  15157  frgpnabllem1  15177  pws1  15415  prdslmodd  15742  psrlmod  16162  znunithash  16534  restcld  16919  clmneg  18595  itg2monolem1  19121  itgconst  19189  dvexp  19318  dvfsumabs  19386  dvtaylp  19765  taylthlem2  19769  tangtx  19889  logsqr  20067  lawcoslem1  20129  chordthmlem2  20146  chordthmlem4  20148  tanatan  20231  atanbndlem  20237  amgmlem  20300  basellem3  20336  basellem5  20338  dvdsmulf1o  20450  chtub  20467  fsumvma  20468  lgsquad2lem1  20613  2sqlem8  20627  dchrmusum2  20659  logsqvma  20707  pntrlog2bndlem4  20745  gxsuc  20955  gxnn0add  20957  vc0  21141  hvsubdistr2  21645  adjlnop  22682  adjcoi  22696  cnvbraval  22706  xrge0pluscn  23337  cvmliftlem6  23836  cvmliftlem10  23840  cvmlift2lem3  23851  faclimlem9  24125  brbtwn2  24605  ax5seglem1  24628  axcontlem2  24665  axcontlem4  24667  bpolydiflem  24861  rltrran  25517  mslb1  25710  heibor  26648  ghomdiv  26677  frlmlbs  27352  proot1ex  27623  sigarperm  27953  sinhpcosh  28464  bnj553  29246  3atlem1  30294  atmod3i2  30676  trljat2  30978  cdleme1  31038  cdlemh2  31627  dihglblem3N  32107  dih1dimatlem0  32140  djhlsmcl  32226  mapdpglem30  32514  hdmapneg  32661  hgmapval1  32708  hgmapmul  32710
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