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

Theorem 3eqtr3rd 2694
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 2687 . 2 (𝜑𝐵 = 𝐶)
51, 4eqtr3d 2687 1 (𝜑𝐷 = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644
This theorem is referenced by:  iunxdif3  4638  fcofo  6583  fcof1oinvd  6588  cantnfp1lem3  8615  fin1a2lem7  9266  prlem934  9893  addid2  10257  addcom  10260  addcomd  10276  negeu  10309  add20  10578  2halves  11298  bcnn  13139  bcpasc  13148  hashfun  13262  wrdeqs1cat  13520  sqreulem  14143  summolem3  14489  fsumneg  14563  geolim  14645  geolim2  14646  mertens  14662  prodmolem3  14707  fallrisefac  14800  bpoly3  14833  sincossq  14950  demoivre  14974  eirrlem  14976  oddpwp1fsum  15162  sadeq  15241  gcdid  15295  phiprmpw  15528  pythagtriplem12  15578  expnprm  15653  fullresc  16558  grpinvid1  17517  grpnpcan  17554  grplactcnv  17565  ghmgrp  17586  conjghm  17738  odmodnn0  18005  gex1  18052  sylow3lem3  18090  efgredeu  18211  odadd2  18298  gsumval3  18354  pgpfac1lem3a  18521  ringnegl  18640  rngnegr  18641  ringmneg2  18643  lmodfopne  18949  lmodvsneg  18955  lss0v  19064  lssvs0or  19158  lvecinv  19161  lspabs2  19168  mplcoe3  19514  mplcoe5  19516  evlvar  19577  zringunit  19884  zringcyg  19887  mdetrlin  20456  mdetunilem6  20471  cramerimplem3  20539  cramerimp  20540  paste  21146  tuslem  22118  tususs  22121  ngpds  22455  ioo2bl  22643  ipcau2  23079  dvexp3  23786  rolle  23798  cmvth  23799  dv11cn  23809  lhop  23824  itgsubstlem  23856  ply1divex  23941  fta1glem1  23970  fta1g  23972  dgrnznn  24048  fta1  24108  vieta1lem2  24111  aaliou2  24140  dvtaylp  24169  dvntaylp  24170  taylthlem1  24172  taylthlem2  24173  dvradcnv  24220  ptolemy  24293  coskpi  24317  tanregt0  24330  cxpeq  24543  isosctrlem2  24594  chordthmlem  24604  dcubic  24618  quart1lem  24627  tanatan  24691  atantan  24695  dvatan  24707  birthdaylem2  24724  rlimcxp  24745  jensenlem2  24759  logdiflbnd  24766  emcllem2  24768  lgamgulmlem2  24801  lgamcvg2  24826  basellem8  24859  bclbnd  25050  lgsqr  25121  lgseisenlem3  25147  lgseisenlem4  25148  lgsquadlem1  25150  lgsquadlem2  25151  rpvmasumlem  25221  dchrisumlem1  25223  dchrisum0flblem1  25242  dchrisum0flblem2  25243  dchrisum0re  25247  dchrisum0lem1  25250  mudivsum  25264  mulogsum  25266  vmalogdivsum2  25272  logsqvma2  25277  selberg2lem  25284  logdivbnd  25290  selbergr  25302  selberg3r  25303  pntrlog2bndlem4  25314  pntrlog2bndlem5  25315  pntpbnd2  25321  miduniq  25625  krippenlem  25630  colperpexlem2  25668  ttgcontlem1  25810  brbtwn2  25830  colinearalglem4  25834  axsegconlem9  25850  ax5seglem1  25853  axbtwnid  25864  axeuclidlem  25887  axcontlem2  25890  axcontlem4  25892  clwwlkel  27009  grpoinvid1  27510  vcz  27558  hosubsub4  28805  lnop0  28953  branmfn  29092  difico  29673  omndmul2  29840  rdivmuldivd  29919  kerunit  29951  carsggect  30508  carsgclctunlem2  30509  ballotlemfrceq  30718  ballotlemrinv0  30722  wrdsplex  30746  hashreprin  30826  hgt750lemb  30862  faclimlem1  31755  poimirlem4  33543  poimirlem23  33562  mblfinlem2  33577  voliunnfl  33583  volsupnfl  33584  itg2addnclem3  33593  ftc2nc  33624  dvasin  33626  areacirclem1  33630  areacirclem4  33633  rngonegmn1l  33870  rngonegmn1r  33871  lfl0  34670  latmassOLD  34834  omlmod1i2N  34865  llnexchb2lem  35472  dalawlem3  35477  pmapj2N  35533  osumcllem9N  35568  pexmidlem6N  35579  4atexlemc  35673  cdleme1  35832  cdleme42a  36076  cdlemg13a  36256  cdlemh2  36421  cdlemk1  36436  tendocnv  36627  dihmeetlem12N  36924  dihmeetlem16N  36928  dihmeetlem19N  36931  dochsatshp  37057  dochexmidlem6  37071  mapdval4N  37238  mapdpglem28  37307  mapdpglem31  37309  mapdindp4  37329  hdmap14lem1a  37475  hdmapinvlem4  37530  irrapxlem5  37707  pellfund14  37779  rmxdbl  37821  jm2.22  37879  itgpowd  38117  0ellimcdiv  40199  fourierdlem95  40736  etransclem46  40815  sigariz  41373  altgsumbc  42455  blengt1fldiv2p1  42712
  Copyright terms: Public domain W3C validator