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

Theorem 3eqtr3rd 2337
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 2330 . 2  |-  ( ph  ->  B  =  C )
51, 4eqtr3d 2330 1  |-  ( ph  ->  D  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632
This theorem is referenced by:  fcofo  5814  fcof1o  5819  cantnfp1lem3  7398  fin1a2lem7  8048  prlem934  8673  addid2  9011  addcom  9014  addcomd  9030  negeu  9058  add20  9302  2halves  9956  bcnn  11340  bcpasc  11349  hashfun  11405  wrdeqs1cat  11491  sqreulem  11859  summolem3  12203  fsumneg  12265  geolim  12342  geolim2  12343  mertens  12358  sincossq  12472  demoivre  12496  eirrlem  12498  sadeq  12679  gcdid  12726  phiprmpw  12860  pythagtriplem12  12895  expnprm  12966  fullresc  13741  grpinvid1  14546  grpnpcan  14573  grplactcnv  14580  conjghm  14729  odmodnn0  14871  gex1  14918  sylow3lem3  14956  efgredeu  15077  odadd2  15157  gsumval3  15207  pgpfac1lem3a  15327  rngnegl  15396  rngnegr  15397  rngmneg2  15399  lmodvsneg  15685  lss0v  15789  lssvs0or  15879  lvecinv  15882  lspabs2  15889  mplcoe3  16226  mplcoe2  16227  zrngunit  16454  zcyg  16461  paste  17038  ngpds  18141  ioo2bl  18315  ipcau2  18680  dvexp3  19341  rolle  19353  cmvth  19354  dv11cn  19364  lhop  19379  itgsubstlem  19411  ply1divex  19538  fta1glem1  19567  fta1g  19569  fta1  19704  vieta1lem2  19707  aaliou2  19736  dvtaylp  19765  dvntaylp  19766  taylthlem1  19768  taylthlem2  19769  dvradcnv  19813  ptolemy  19880  coskpi  19904  tanregt0  19917  cxpeq  20113  isosctrlem2  20135  chordthmlem  20145  dcubic  20158  quart1lem  20167  tanatan  20231  atantan  20235  dvatan  20247  birthdaylem2  20263  rlimcxp  20284  jensenlem2  20298  emcllem2  20306  basellem8  20341  bclbnd  20535  lgsqr  20601  lgseisenlem3  20606  lgseisenlem4  20607  lgsquadlem1  20609  lgsquadlem2  20610  rpvmasumlem  20652  dchrisumlem1  20654  dchrisum0flblem1  20673  dchrisum0flblem2  20674  dchrisum0re  20678  dchrisum0lem1  20681  mudivsum  20695  mulogsum  20697  vmalogdivsum2  20703  logsqvma2  20708  selberg2lem  20715  logdivbnd  20721  selbergr  20733  selberg3r  20734  pntrlog2bndlem4  20745  pntrlog2bndlem5  20746  pntpbnd2  20752  grpoinvid1  20913  vcz  21142  hosubsub4  22414  lnop0  22562  branmfn  22701  ballotlemfrceq  23103  ballotlemrinv0  23107  faclimlem5  24121  prodmolem3  24156  brbtwn2  24605  colinearalglem4  24609  axsegconlem9  24625  ax5seglem1  24628  axbtwnid  24639  axeuclidlem  24662  axcontlem2  24665  axcontlem4  24667  bpoly3  24865  dvreasin  25026  areacirclem2  25028  areacirclem5  25032  fprodsub  25482  cnegvex2  25763  rngonegmn1l  26683  rngonegmn1r  26684  irrapxlem5  27014  pellfund14  27086  rmxdbl  27127  jm2.22  27191  dgrnznn  27443  sigariz  27956  lfl0  29877  latmassOLD  30041  omlmod1i2N  30072  llnexchb2lem  30679  dalawlem3  30684  pmapj2N  30740  osumcllem9N  30775  pexmidlem6N  30786  4atexlemc  30880  cdleme1  31038  cdleme42a  31282  cdlemg13a  31462  cdlemh2  31627  cdlemk1  31642  tendocnv  31833  dihmeetlem12N  32130  dihmeetlem16N  32134  dihmeetlem19N  32137  dochsatshp  32263  dochexmidlem6  32277  mapdval4N  32444  mapdpglem28  32513  mapdpglem31  32515  mapdindp4  32535  hdmap14lem1a  32681  hdmapinvlem4  32736
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