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

Theorem 3eqtr3rd 2849
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 2842 . 2 (𝜑𝐵 = 𝐶)
51, 4eqtr3d 2842 1 (𝜑𝐷 = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-cleq 2799
This theorem is referenced by:  iunxdif3  4798  fcofo  6763  fcof1oinvd  6768  cantnfp1lem3  8820  fin1a2lem7  9509  prlem934  10136  addid2  10500  addcom  10503  addcomd  10519  negeu  10552  add20  10821  2halves  11523  bcnn  13315  bcpasc  13324  hashfun  13437  wrdeqs1cat  13694  sqreulem  14318  summolem3  14664  fsumneg  14737  geolim  14819  geolim2  14820  mertens  14835  prodmolem3  14880  fallrisefac  14972  bpoly3  15005  sincossq  15122  demoivre  15146  eirrlem  15148  oddpwp1fsum  15331  sadeq  15409  gcdid  15463  phiprmpw  15694  pythagtriplem12  15744  expnprm  15819  fullresc  16711  grpinvid1  17671  grpnpcan  17708  grplactcnv  17719  ghmgrp  17740  conjghm  17889  odmodnn0  18156  gex1  18203  sylow3lem3  18241  efgredeu  18362  odadd2  18449  gsumval3  18505  pgpfac1lem3a  18673  ringnegl  18792  rngnegr  18793  ringmneg2  18795  lmodfopne  19101  lmodvsneg  19107  lss0v  19219  lssvs0or  19313  lvecinv  19316  lspabs2  19323  mplcoe3  19671  mplcoe5  19673  evlvar  19733  zringunit  20040  zringcyg  20043  mdetrlin  20615  mdetunilem6  20630  cramerimplem3  20700  cramerimp  20701  paste  21308  tuslem  22280  tususs  22283  ngpds  22617  ioo2bl  22805  ipcau2  23241  dvexp3  23951  rolle  23963  cmvth  23964  dv11cn  23974  lhop  23989  itgsubstlem  24021  ply1divex  24106  fta1glem1  24135  fta1g  24137  dgrnznn  24213  fta1  24273  vieta1lem2  24276  aaliou2  24305  dvtaylp  24334  dvntaylp  24335  taylthlem1  24337  taylthlem2  24338  dvradcnv  24385  ptolemy  24459  coskpi  24483  tanregt0  24496  cxpeq  24708  isosctrlem2  24759  chordthmlem  24769  dcubic  24783  quart1lem  24792  tanatan  24856  atantan  24860  dvatan  24872  birthdaylem2  24889  rlimcxp  24910  jensenlem2  24924  logdiflbnd  24931  emcllem2  24933  lgamgulmlem2  24966  lgamcvg2  24991  basellem8  25024  bclbnd  25215  lgsqr  25286  lgseisenlem3  25312  lgseisenlem4  25313  lgsquadlem1  25315  lgsquadlem2  25316  rpvmasumlem  25386  dchrisumlem1  25388  dchrisum0flblem1  25407  dchrisum0flblem2  25408  dchrisum0re  25412  dchrisum0lem1  25415  mudivsum  25429  mulogsum  25431  vmalogdivsum2  25437  logsqvma2  25442  selberg2lem  25449  logdivbnd  25455  selbergr  25467  selberg3r  25468  pntrlog2bndlem4  25479  pntrlog2bndlem5  25480  pntpbnd2  25486  miduniq  25790  krippenlem  25795  colperpexlem2  25833  ttgcontlem1  25975  brbtwn2  25995  colinearalglem4  25999  axsegconlem9  26015  ax5seglem1  26018  axbtwnid  26029  axeuclidlem  26052  axcontlem2  26055  axcontlem4  26057  clwwlkel  27191  grpoinvid1  27707  vcz  27754  hosubsub4  29001  lnop0  29149  branmfn  29288  difico  29868  omndmul2  30033  rdivmuldivd  30112  kerunit  30144  carsggect  30701  carsgclctunlem2  30702  ballotlemfrceq  30911  ballotlemrinv0  30915  wrdsplex  30939  hashreprin  31019  hgt750lemb  31055  faclimlem1  31946  poimirlem4  33721  poimirlem23  33740  mblfinlem2  33755  voliunnfl  33761  volsupnfl  33762  itg2addnclem3  33770  ftc2nc  33801  dvasin  33803  areacirclem1  33807  areacirclem4  33810  rngonegmn1l  34046  rngonegmn1r  34047  lfl0  34840  latmassOLD  35004  omlmod1i2N  35035  llnexchb2lem  35643  dalawlem3  35648  pmapj2N  35704  osumcllem9N  35739  pexmidlem6N  35750  4atexlemc  35844  cdleme1  36002  cdleme42a  36246  cdlemg13a  36426  cdlemh2  36591  cdlemk1  36606  tendocnv  36796  dihmeetlem12N  37093  dihmeetlem16N  37097  dihmeetlem19N  37100  dochsatshp  37226  dochexmidlem6  37240  mapdval4N  37407  mapdpglem28  37476  mapdpglem31  37478  mapdindp4  37498  hdmap14lem1a  37641  hdmapinvlem4  37696  irrapxlem5  37886  pellfund14  37958  rmxdbl  37999  jm2.22  38057  itgpowd  38294  0ellimcdiv  40355  fourierdlem95  40891  etransclem46  40970  sigariz  41528  altgsumbc  42692  blengt1fldiv2p1  42949
  Copyright terms: Public domain W3C validator