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

Theorem 3eqtr3rd 2445
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 2438 . 2  |-  ( ph  ->  B  =  C )
51, 4eqtr3d 2438 1  |-  ( ph  ->  D  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649
This theorem is referenced by:  fcofo  5980  fcof1o  5985  cantnfp1lem3  7592  fin1a2lem7  8242  prlem934  8866  addid2  9205  addcom  9208  addcomd  9224  negeu  9252  add20  9496  2halves  10152  bcnn  11558  bcpasc  11567  hashfun  11655  wrdeqs1cat  11744  sqreulem  12118  summolem3  12463  fsumneg  12525  geolim  12602  geolim2  12603  mertens  12618  sincossq  12732  demoivre  12756  eirrlem  12758  sadeq  12939  gcdid  12986  phiprmpw  13120  pythagtriplem12  13155  expnprm  13226  fullresc  14003  grpinvid1  14808  grpnpcan  14835  grplactcnv  14842  conjghm  14991  odmodnn0  15133  gex1  15180  sylow3lem3  15218  efgredeu  15339  odadd2  15419  gsumval3  15469  pgpfac1lem3a  15589  rngnegl  15658  rngnegr  15659  rngmneg2  15661  lmodvsneg  15943  lss0v  16047  lssvs0or  16137  lvecinv  16140  lspabs2  16147  mplcoe3  16484  mplcoe2  16485  zrngunit  16720  zcyg  16727  paste  17312  tuslem  18250  tususs  18253  ngpds  18603  ioo2bl  18777  ipcau2  19144  cmetcusp  19261  dvexp3  19815  rolle  19827  cmvth  19828  dv11cn  19838  lhop  19853  itgsubstlem  19885  ply1divex  20012  fta1glem1  20041  fta1g  20043  fta1  20178  vieta1lem2  20181  aaliou2  20210  dvtaylp  20239  dvntaylp  20240  taylthlem1  20242  taylthlem2  20243  dvradcnv  20290  ptolemy  20357  coskpi  20381  tanregt0  20394  cxpeq  20594  isosctrlem2  20616  chordthmlem  20626  dcubic  20639  quart1lem  20648  tanatan  20712  atantan  20716  dvatan  20728  birthdaylem2  20744  rlimcxp  20765  jensenlem2  20779  logdiflbnd  20786  emcllem2  20788  basellem8  20823  bclbnd  21017  lgsqr  21083  lgseisenlem3  21088  lgseisenlem4  21089  lgsquadlem1  21091  lgsquadlem2  21092  rpvmasumlem  21134  dchrisumlem1  21136  dchrisum0flblem1  21155  dchrisum0flblem2  21156  dchrisum0re  21160  dchrisum0lem1  21163  mudivsum  21177  mulogsum  21179  vmalogdivsum2  21185  logsqvma2  21190  selberg2lem  21197  logdivbnd  21203  selbergr  21215  selberg3r  21216  pntrlog2bndlem4  21227  pntrlog2bndlem5  21228  pntpbnd2  21234  grpoinvid1  21771  vcz  22002  hosubsub4  23274  lnop0  23422  branmfn  23561  difico  24099  rdivmuldivd  24180  kerunit  24214  ballotlemfrceq  24739  ballotlemrinv0  24743  lgamgulmlem2  24767  lgamcvg2  24792  prodmolem3  25212  fallrisefac  25293  faclimlem1  25310  brbtwn2  25748  colinearalglem4  25752  axsegconlem9  25768  ax5seglem1  25771  axbtwnid  25782  axeuclidlem  25805  axcontlem2  25808  axcontlem4  25810  bpoly3  26008  mblfinlem  26143  voliunnfl  26149  volsupnfl  26150  itg2addnclem3  26157  dvreasin  26179  areacirclem2  26181  areacirclem5  26185  rngonegmn1l  26455  rngonegmn1r  26456  irrapxlem5  26779  pellfund14  26851  rmxdbl  26892  jm2.22  26956  dgrnznn  27208  sigariz  27720  lfl0  29548  latmassOLD  29712  omlmod1i2N  29743  llnexchb2lem  30350  dalawlem3  30355  pmapj2N  30411  osumcllem9N  30446  pexmidlem6N  30457  4atexlemc  30551  cdleme1  30709  cdleme42a  30953  cdlemg13a  31133  cdlemh2  31298  cdlemk1  31313  tendocnv  31504  dihmeetlem12N  31801  dihmeetlem16N  31805  dihmeetlem19N  31808  dochsatshp  31934  dochexmidlem6  31948  mapdval4N  32115  mapdpglem28  32184  mapdpglem31  32186  mapdindp4  32206  hdmap14lem1a  32352  hdmapinvlem4  32407
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2397
  Copyright terms: Public domain W3C validator