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

Theorem 3eqtr3rd 2476
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 2469 . 2  |-  ( ph  ->  B  =  C )
51, 4eqtr3d 2469 1  |-  ( ph  ->  D  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652
This theorem is referenced by:  fcofo  6013  fcof1o  6018  cantnfp1lem3  7628  fin1a2lem7  8278  prlem934  8902  addid2  9241  addcom  9244  addcomd  9260  negeu  9288  add20  9532  2halves  10188  bcnn  11595  bcpasc  11604  hashfun  11692  wrdeqs1cat  11781  sqreulem  12155  summolem3  12500  fsumneg  12562  geolim  12639  geolim2  12640  mertens  12655  sincossq  12769  demoivre  12793  eirrlem  12795  sadeq  12976  gcdid  13023  phiprmpw  13157  pythagtriplem12  13192  expnprm  13263  fullresc  14040  grpinvid1  14845  grpnpcan  14872  grplactcnv  14879  conjghm  15028  odmodnn0  15170  gex1  15217  sylow3lem3  15255  efgredeu  15376  odadd2  15456  gsumval3  15506  pgpfac1lem3a  15626  rngnegl  15695  rngnegr  15696  rngmneg2  15698  lmodvsneg  15980  lss0v  16084  lssvs0or  16174  lvecinv  16177  lspabs2  16184  mplcoe3  16521  mplcoe2  16522  zrngunit  16757  zcyg  16764  paste  17350  tuslem  18289  tususs  18292  ngpds  18642  ioo2bl  18816  ipcau2  19183  cmetcusp  19300  dvexp3  19854  rolle  19866  cmvth  19867  dv11cn  19877  lhop  19892  itgsubstlem  19924  ply1divex  20051  fta1glem1  20080  fta1g  20082  fta1  20217  vieta1lem2  20220  aaliou2  20249  dvtaylp  20278  dvntaylp  20279  taylthlem1  20281  taylthlem2  20282  dvradcnv  20329  ptolemy  20396  coskpi  20420  tanregt0  20433  cxpeq  20633  isosctrlem2  20655  chordthmlem  20665  dcubic  20678  quart1lem  20687  tanatan  20751  atantan  20755  dvatan  20767  birthdaylem2  20783  rlimcxp  20804  jensenlem2  20818  logdiflbnd  20825  emcllem2  20827  basellem8  20862  bclbnd  21056  lgsqr  21122  lgseisenlem3  21127  lgseisenlem4  21128  lgsquadlem1  21130  lgsquadlem2  21131  rpvmasumlem  21173  dchrisumlem1  21175  dchrisum0flblem1  21194  dchrisum0flblem2  21195  dchrisum0re  21199  dchrisum0lem1  21202  mudivsum  21216  mulogsum  21218  vmalogdivsum2  21224  logsqvma2  21229  selberg2lem  21236  logdivbnd  21242  selbergr  21254  selberg3r  21255  pntrlog2bndlem4  21266  pntrlog2bndlem5  21267  pntpbnd2  21273  grpoinvid1  21810  vcz  22041  hosubsub4  23313  lnop0  23461  branmfn  23600  difico  24138  rdivmuldivd  24219  kerunit  24253  ballotlemfrceq  24778  ballotlemrinv0  24782  lgamgulmlem2  24806  lgamcvg2  24831  prodmolem3  25251  fallrisefac  25333  faclimlem1  25354  brbtwn2  25836  colinearalglem4  25840  axsegconlem9  25856  ax5seglem1  25859  axbtwnid  25870  axeuclidlem  25893  axcontlem2  25896  axcontlem4  25898  bpoly3  26096  mblfinlem  26234  voliunnfl  26240  volsupnfl  26241  itg2addnclem3  26248  ftc2nc  26279  dvreasin  26280  areacirclem2  26282  areacirclem5  26286  rngonegmn1l  26556  rngonegmn1r  26557  irrapxlem5  26880  pellfund14  26952  rmxdbl  26993  jm2.22  27057  dgrnznn  27308  sigariz  27820  lfl0  29800  latmassOLD  29964  omlmod1i2N  29995  llnexchb2lem  30602  dalawlem3  30607  pmapj2N  30663  osumcllem9N  30698  pexmidlem6N  30709  4atexlemc  30803  cdleme1  30961  cdleme42a  31205  cdlemg13a  31385  cdlemh2  31550  cdlemk1  31565  tendocnv  31756  dihmeetlem12N  32053  dihmeetlem16N  32057  dihmeetlem19N  32060  dochsatshp  32186  dochexmidlem6  32200  mapdval4N  32367  mapdpglem28  32436  mapdpglem31  32438  mapdindp4  32458  hdmap14lem1a  32604  hdmapinvlem4  32659
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-cleq 2428
  Copyright terms: Public domain W3C validator