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

Theorem 3eqtr3rd 2504
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 2497 . 2  |-  ( ph  ->  B  =  C )
51, 4eqtr3d 2497 1  |-  ( ph  ->  D  =  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-cleq 2446
This theorem is referenced by:  fcofo  6102  fcof1o  6107  cantnfp1lem3  8000  cantnfp1lem3OLD  8026  fin1a2lem7  8687  prlem934  9314  addid2  9664  addcom  9667  addcomd  9683  negeu  9712  add20  9963  2halves  10665  bcnn  12206  bcpasc  12215  hashfun  12318  wrdeqs1cat  12488  sqreulem  12966  summolem3  13310  fsumneg  13373  geolim  13449  geolim2  13450  mertens  13465  sincossq  13579  demoivre  13603  eirrlem  13605  sadeq  13787  gcdid  13834  phiprmpw  13970  pythagtriplem12  14012  expnprm  14083  fullresc  14881  grpinvid1  15706  grpnpcan  15737  grplactcnv  15744  conjghm  15897  odmodnn0  16165  gex1  16212  sylow3lem3  16250  efgredeu  16371  odadd2  16453  gsumval3OLD  16504  gsumval3  16507  pgpfac1lem3a  16700  rngnegl  16809  rngnegr  16810  rngmneg2  16812  lmodvsneg  17113  lss0v  17221  lssvs0or  17315  lvecinv  17318  lspabs2  17325  mplcoe3  17670  mplcoe3OLD  17671  mplcoe5  17673  mplcoe2OLD  17675  evlvar  17740  zringcyg  18033  zcyg  18038  zringunit  18040  zrngunit  18041  mdetrlin  18541  mdetunilem6  18556  cramerimplem3  18624  cramerimp  18625  paste  19031  tuslem  19975  tususs  19978  ngpds  20328  ioo2bl  20503  ipcau2  20882  cmetcusp  20999  dvexp3  21584  rolle  21596  cmvth  21597  dv11cn  21607  lhop  21622  itgsubstlem  21654  ply1divex  21742  fta1glem1  21771  fta1g  21773  fta1  21908  vieta1lem2  21911  aaliou2  21940  dvtaylp  21969  dvntaylp  21970  taylthlem1  21972  taylthlem2  21973  dvradcnv  22020  ptolemy  22092  coskpi  22116  tanregt0  22129  cxpeq  22329  isosctrlem2  22351  chordthmlem  22361  dcubic  22375  quart1lem  22384  tanatan  22448  atantan  22452  dvatan  22464  birthdaylem2  22480  rlimcxp  22501  jensenlem2  22515  logdiflbnd  22522  emcllem2  22524  basellem8  22559  bclbnd  22753  lgsqr  22819  lgseisenlem3  22824  lgseisenlem4  22825  lgsquadlem1  22827  lgsquadlem2  22828  rpvmasumlem  22870  dchrisumlem1  22872  dchrisum0flblem1  22891  dchrisum0flblem2  22892  dchrisum0re  22896  dchrisum0lem1  22899  mudivsum  22913  mulogsum  22915  vmalogdivsum2  22921  logsqvma2  22926  selberg2lem  22933  logdivbnd  22939  selbergr  22951  selberg3r  22952  pntrlog2bndlem4  22963  pntrlog2bndlem5  22964  pntpbnd2  22970  miduniq2  23225  krippenlem  23228  colperplem2  23259  ttgcontlem1  23284  brbtwn2  23304  colinearalglem4  23308  axsegconlem9  23324  ax5seglem1  23327  axbtwnid  23338  axeuclidlem  23361  axcontlem2  23364  axcontlem4  23366  grpoinvid1  23870  vcz  24101  hosubsub4  25375  lnop0  25523  branmfn  25662  difico  26219  omndmul2  26321  rdivmuldivd  26405  kerunit  26437  ballotlemfrceq  27056  ballotlemrinv0  27060  wrdsplex  27084  lgamgulmlem2  27161  lgamcvg2  27186  prodmolem3  27591  fallrisefac  27673  faclimlem1  27694  bpoly3  28346  mblfinlem2  28578  voliunnfl  28584  volsupnfl  28585  itg2addnclem3  28594  ftc2nc  28625  dvasin  28629  areacirclem1  28633  areacirclem4  28636  rngonegmn1l  28904  rngonegmn1r  28905  irrapxlem5  29316  pellfund14  29388  rmxdbl  29429  jm2.22  29493  dgrnznn  29641  itgpowd  29739  sigariz  30048  clwwlkel  30604  altgsumbc  30898  lfl0  33049  latmassOLD  33213  omlmod1i2N  33244  llnexchb2lem  33851  dalawlem3  33856  pmapj2N  33912  osumcllem9N  33947  pexmidlem6N  33958  4atexlemc  34052  cdleme1  34210  cdleme42a  34454  cdlemg13a  34634  cdlemh2  34799  cdlemk1  34814  tendocnv  35005  dihmeetlem12N  35302  dihmeetlem16N  35306  dihmeetlem19N  35309  dochsatshp  35435  dochexmidlem6  35449  mapdval4N  35616  mapdpglem28  35685  mapdpglem31  35687  mapdindp4  35707  hdmap14lem1a  35853  hdmapinvlem4  35908
  Copyright terms: Public domain W3C validator