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

Theorem 3eqtr3rd 2491
Description: A deduction from three chained equalities. (Contributed by NM, 14-Jan-2006.)
Hypotheses
Ref Expression
3eqtr3d.1  |-  ( ph  ->  A  =  B )
3eqtr3d.2  |-  ( ph  ->  A  =  C )
3eqtr3d.3  |-  ( ph  ->  B  =  D )
Assertion
Ref Expression
3eqtr3rd  |-  ( ph  ->  D  =  C )

Proof of Theorem 3eqtr3rd
StepHypRef Expression
1 3eqtr3d.3 . 2  |-  ( ph  ->  B  =  D )
2 3eqtr3d.1 . . 3  |-  ( ph  ->  A  =  B )
3 3eqtr3d.2 . . 3  |-  ( ph  ->  A  =  C )
42, 3eqtr3d 2484 . 2  |-  ( ph  ->  B  =  C )
51, 4eqtr3d 2484 1  |-  ( ph  ->  D  =  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1381
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-cleq 2433
This theorem is referenced by:  fcofo  6172  fcof1oinvd  6177  cantnfp1lem3  8097  cantnfp1lem3OLD  8123  fin1a2lem7  8784  prlem934  9409  addid2  9761  addcom  9764  addcomd  9780  negeu  9810  add20  10065  2halves  10768  bcnn  12364  bcpasc  12373  hashfun  12469  wrdeqs1cat  12674  sqreulem  13166  summolem3  13510  fsumneg  13576  geolim  13653  geolim2  13654  mertens  13669  sincossq  13783  demoivre  13807  eirrlem  13809  sadeq  13994  gcdid  14041  phiprmpw  14178  pythagtriplem12  14222  expnprm  14293  fullresc  15089  grpinvid1  15967  grpnpcan  15999  grplactcnv  16007  ghmgrp  16063  conjghm  16166  odmodnn0  16433  gex1  16480  sylow3lem3  16518  efgredeu  16639  odadd2  16724  gsumval3OLD  16777  gsumval3  16780  pgpfac1lem3a  16995  ringnegl  17108  rngnegr  17109  ringmneg2  17111  lmodvsneg  17422  lss0v  17530  lssvs0or  17624  lvecinv  17627  lspabs2  17634  mplcoe3  17996  mplcoe3OLD  17997  mplcoe5  17999  mplcoe2OLD  18001  evlvar  18066  zringcyg  18380  zcyg  18385  zringunit  18387  zrngunit  18388  mdetrlin  18971  mdetunilem6  18986  cramerimplem3  19054  cramerimp  19055  paste  19661  tuslem  20636  tususs  20639  ngpds  20989  ioo2bl  21164  ipcau2  21543  dvexp3  22245  rolle  22257  cmvth  22258  dv11cn  22268  lhop  22283  itgsubstlem  22315  ply1divex  22403  fta1glem1  22432  fta1g  22434  fta1  22569  vieta1lem2  22572  aaliou2  22601  dvtaylp  22630  dvntaylp  22631  taylthlem1  22633  taylthlem2  22634  dvradcnv  22681  ptolemy  22754  coskpi  22778  tanregt0  22791  cxpeq  22996  isosctrlem2  23018  chordthmlem  23028  dcubic  23042  quart1lem  23051  tanatan  23115  atantan  23119  dvatan  23131  birthdaylem2  23147  rlimcxp  23168  jensenlem2  23182  logdiflbnd  23189  emcllem2  23191  basellem8  23226  bclbnd  23420  lgsqr  23486  lgseisenlem3  23491  lgseisenlem4  23492  lgsquadlem1  23494  lgsquadlem2  23495  rpvmasumlem  23537  dchrisumlem1  23539  dchrisum0flblem1  23558  dchrisum0flblem2  23559  dchrisum0re  23563  dchrisum0lem1  23566  mudivsum  23580  mulogsum  23582  vmalogdivsum2  23588  logsqvma2  23593  selberg2lem  23600  logdivbnd  23606  selbergr  23618  selberg3r  23619  pntrlog2bndlem4  23630  pntrlog2bndlem5  23631  pntpbnd2  23637  miduniq  23927  krippenlem  23932  colperpexlem2  23970  ttgcontlem1  24053  brbtwn2  24073  colinearalglem4  24077  axsegconlem9  24093  ax5seglem1  24096  axbtwnid  24107  axeuclidlem  24130  axcontlem2  24133  axcontlem4  24135  clwwlkel  24658  grpoinvid1  25097  vcz  25328  hosubsub4  26602  lnop0  26750  branmfn  26889  difico  27459  omndmul2  27568  rdivmuldivd  27647  kerunit  27679  ballotlemfrceq  28333  ballotlemrinv0  28337  wrdsplex  28361  lgamgulmlem2  28438  lgamcvg2  28463  prodmolem3  29033  fallrisefac  29115  faclimlem1  29136  bpoly3  29788  mblfinlem2  30020  voliunnfl  30026  volsupnfl  30027  itg2addnclem3  30036  ftc2nc  30067  dvasin  30071  areacirclem1  30075  areacirclem4  30078  rngonegmn1l  30320  rngonegmn1r  30321  irrapxlem5  30730  pellfund14  30802  rmxdbl  30843  jm2.22  30905  dgrnznn  31053  itgpowd  31151  0ellimcdiv  31559  fourierdlem95  31869  sigariz  31914  altgsumbc  32649  lfl0  34492  latmassOLD  34656  omlmod1i2N  34687  llnexchb2lem  35294  dalawlem3  35299  pmapj2N  35355  osumcllem9N  35390  pexmidlem6N  35401  4atexlemc  35495  cdleme1  35654  cdleme42a  35899  cdlemg13a  36079  cdlemh2  36244  cdlemk1  36259  tendocnv  36450  dihmeetlem12N  36747  dihmeetlem16N  36751  dihmeetlem19N  36754  dochsatshp  36880  dochexmidlem6  36894  mapdval4N  37061  mapdpglem28  37130  mapdpglem31  37132  mapdindp4  37152  hdmap14lem1a  37298  hdmapinvlem4  37353
  Copyright terms: Public domain W3C validator