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

Theorem 3eqtr3rd 2663
Description: A deduction from three chained equalities. (Contributed by NM, 14-Jan-2006.)
Hypotheses
Ref Expression
3eqtr3d.1 (𝜑𝐴 = 𝐵)
3eqtr3d.2 (𝜑𝐴 = 𝐶)
3eqtr3d.3 (𝜑𝐵 = 𝐷)
Assertion
Ref Expression
3eqtr3rd (𝜑𝐷 = 𝐶)

Proof of Theorem 3eqtr3rd
StepHypRef Expression
1 3eqtr3d.3 . 2 (𝜑𝐵 = 𝐷)
2 3eqtr3d.1 . . 3 (𝜑𝐴 = 𝐵)
3 3eqtr3d.2 . . 3 (𝜑𝐴 = 𝐶)
42, 3eqtr3d 2656 . 2 (𝜑𝐵 = 𝐶)
51, 4eqtr3d 2656 1 (𝜑𝐷 = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1481
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1703  df-cleq 2613
This theorem is referenced by:  iunxdif3  4597  fcofo  6528  fcof1oinvd  6533  cantnfp1lem3  8562  fin1a2lem7  9213  prlem934  9840  addid2  10204  addcom  10207  addcomd  10223  negeu  10256  add20  10525  2halves  11245  bcnn  13082  bcpasc  13091  hashfun  13207  wrdeqs1cat  13456  sqreulem  14080  summolem3  14426  fsumneg  14500  geolim  14582  geolim2  14583  mertens  14599  prodmolem3  14644  fallrisefac  14737  bpoly3  14770  sincossq  14887  demoivre  14911  eirrlem  14913  oddpwp1fsum  15096  sadeq  15175  gcdid  15229  phiprmpw  15462  pythagtriplem12  15512  expnprm  15587  fullresc  16492  grpinvid1  17451  grpnpcan  17488  grplactcnv  17499  ghmgrp  17520  conjghm  17672  odmodnn0  17940  gex1  17987  sylow3lem3  18025  efgredeu  18146  odadd2  18233  gsumval3  18289  pgpfac1lem3a  18456  ringnegl  18575  rngnegr  18576  ringmneg2  18578  lmodfopne  18882  lmodvsneg  18888  lss0v  18997  lssvs0or  19091  lvecinv  19094  lspabs2  19101  mplcoe3  19447  mplcoe5  19449  evlvar  19510  zringunit  19817  zringcyg  19820  mdetrlin  20389  mdetunilem6  20404  cramerimplem3  20472  cramerimp  20473  paste  21079  tuslem  22052  tususs  22055  ngpds  22389  ioo2bl  22577  ipcau2  23014  dvexp3  23722  rolle  23734  cmvth  23735  dv11cn  23745  lhop  23760  itgsubstlem  23792  ply1divex  23877  fta1glem1  23906  fta1g  23908  dgrnznn  23984  fta1  24044  vieta1lem2  24047  aaliou2  24076  dvtaylp  24105  dvntaylp  24106  taylthlem1  24108  taylthlem2  24109  dvradcnv  24156  ptolemy  24229  coskpi  24253  tanregt0  24266  cxpeq  24479  isosctrlem2  24530  chordthmlem  24540  dcubic  24554  quart1lem  24563  tanatan  24627  atantan  24631  dvatan  24643  birthdaylem2  24660  rlimcxp  24681  jensenlem2  24695  logdiflbnd  24702  emcllem2  24704  lgamgulmlem2  24737  lgamcvg2  24762  basellem8  24795  bclbnd  24986  lgsqr  25057  lgseisenlem3  25083  lgseisenlem4  25084  lgsquadlem1  25086  lgsquadlem2  25087  rpvmasumlem  25157  dchrisumlem1  25159  dchrisum0flblem1  25178  dchrisum0flblem2  25179  dchrisum0re  25183  dchrisum0lem1  25186  mudivsum  25200  mulogsum  25202  vmalogdivsum2  25208  logsqvma2  25213  selberg2lem  25220  logdivbnd  25226  selbergr  25238  selberg3r  25239  pntrlog2bndlem4  25250  pntrlog2bndlem5  25251  pntpbnd2  25257  miduniq  25561  krippenlem  25566  colperpexlem2  25604  ttgcontlem1  25746  brbtwn2  25766  colinearalglem4  25770  axsegconlem9  25786  ax5seglem1  25789  axbtwnid  25800  axeuclidlem  25823  axcontlem2  25826  axcontlem4  25828  clwwlksel  26894  grpoinvid1  27352  vcz  27400  hosubsub4  28647  lnop0  28795  branmfn  28934  difico  29519  omndmul2  29686  rdivmuldivd  29765  kerunit  29797  carsggect  30354  carsgclctunlem2  30355  ballotlemfrceq  30564  ballotlemrinv0  30568  wrdsplex  30592  hashreprin  30672  hgt750lemb  30708  faclimlem1  31604  poimirlem4  33384  poimirlem23  33403  mblfinlem2  33418  voliunnfl  33424  volsupnfl  33425  itg2addnclem3  33434  ftc2nc  33465  dvasin  33467  areacirclem1  33471  areacirclem4  33474  rngonegmn1l  33711  rngonegmn1r  33712  lfl0  34171  latmassOLD  34335  omlmod1i2N  34366  llnexchb2lem  34973  dalawlem3  34978  pmapj2N  35034  osumcllem9N  35069  pexmidlem6N  35080  4atexlemc  35174  cdleme1  35333  cdleme42a  35578  cdlemg13a  35758  cdlemh2  35923  cdlemk1  35938  tendocnv  36129  dihmeetlem12N  36426  dihmeetlem16N  36430  dihmeetlem19N  36433  dochsatshp  36559  dochexmidlem6  36573  mapdval4N  36740  mapdpglem28  36809  mapdpglem31  36811  mapdindp4  36831  hdmap14lem1a  36977  hdmapinvlem4  37032  irrapxlem5  37209  pellfund14  37281  rmxdbl  37323  jm2.22  37381  itgpowd  37619  0ellimcdiv  39681  fourierdlem95  40181  etransclem46  40260  sigariz  40815  altgsumbc  41895  blengt1fldiv2p1  42152
  Copyright terms: Public domain W3C validator