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

Theorem 3eqtr3d 2848
Description: A deduction from three chained equalities. (Contributed by NM, 4-Aug-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
3eqtr3d.1 (𝜑𝐴 = 𝐵)
3eqtr3d.2 (𝜑𝐴 = 𝐶)
3eqtr3d.3 (𝜑𝐵 = 𝐷)
Assertion
Ref Expression
3eqtr3d (𝜑𝐶 = 𝐷)

Proof of Theorem 3eqtr3d
StepHypRef Expression
1 3eqtr3d.1 . . 3 (𝜑𝐴 = 𝐵)
2 3eqtr3d.2 . . 3 (𝜑𝐴 = 𝐶)
31, 2eqtr3d 2842 . 2 (𝜑𝐵 = 𝐶)
4 3eqtr3d.3 . 2 (𝜑𝐵 = 𝐷)
53, 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:  mpteqb  6516  fvmptt  6517  fsnunfv  6674  f1ocnvfv1  6752  f1ocnvfv2  6753  fcof1  6762  weniso  6824  caov12d  7081  caov13d  7083  caov411d  7085  caovmo  7097  grprinvlem  7098  grprinvd  7099  grpridd  7100  onovuni  7671  tfrlem5  7708  seqomlem1  7777  seqomlem4  7780  onasuc  7841  onesuc  7843  oeeui  7915  fopwdom  8303  unxpdomlem2  8400  cantnfres  8817  cnfcom2lem  8841  cnfcom2  8842  updjud  9039  cardiun  9087  ackbij1lem16  9338  ackbij2lem2  9343  fpwwe2lem6  9738  fpwwe2lem8  9740  canthp1lem2  9756  mul12  10483  mul4  10486  addid1  10497  addcan  10501  addcom  10503  addcomd  10519  add12  10534  ppncan  10604  addsub4  10605  subaddeqd  10727  muladd  10743  mulcand  10941  receu  10953  div13  10987  divdivdiv  11007  divcan5  11008  divdiv1  11017  divdiv2  11018  halfaddsub  11528  xadddi  12339  xov1plusxeqvd  12537  fztp  12616  flzadd  12847  fldiv  12879  mulp1mod1  12931  modnegd  12945  modsub12d  12947  2submod  12951  seqm1  13037  seqcaopr  13057  seqf1o  13061  exprec  13120  expsub  13127  zesq  13206  digit1  13217  discr1  13219  discr  13220  facnn2  13285  faclbnd6  13302  hashfz1  13350  hashdom  13382  hashun  13385  hashbclem  13449  hashfac  13455  seqcoll  13461  ccatopth  13690  repsw2  13914  repsw3  13915  shftval3  14035  crre  14073  resub  14086  imsub  14094  cjsub  14108  abslem2  14298  sqreulem  14318  climshft2  14532  isercolllem2  14615  iseraltlem2  14632  iseraltlem3  14633  fsumsub  14738  telfsumo  14752  telfsumo2  14753  hashiun  14772  bcxmas  14785  climcndslem1  14799  climcndslem2  14800  trireciplem  14812  geoser  14817  geo2sum2  14823  fprodm1  14914  fallfacfwd  14983  binomfallfaclem2  14987  bpolydiflem  15001  bpoly4  15006  fsumcube  15007  sinsub  15114  cossub  15115  rpnnen2lem10  15168  ruclem12  15186  p1modz1  15206  mod2eq1n2dvds  15287  pwp1fsum  15330  divalglem9  15340  bitsinv1lem  15378  bitsinv1  15379  bitsf1  15383  sadasslem  15407  bitsres  15410  smup1  15426  smumul  15430  modgcd  15468  absmulgcd  15481  gcdmultiplez  15485  eucalg  15515  lcmgcd  15535  lcmid  15537  lcmftp  15564  numdensq  15675  dfphi2  15692  phiprm  15695  fermltl  15702  prmdiveq  15704  hashgcdlem  15706  odzdvds  15713  powm2modprm  15721  modprm0  15723  coprimeprodsq  15726  pythagtriplem6  15739  pythagtriplem7  15740  pythagtriplem12  15744  pythagtriplem16  15748  pcaddlem  15805  sumhash  15813  pcfac  15816  pockthlem  15822  prmreclem6  15838  4sqlem12  15873  4sqlem15  15876  vdwlem3  15900  vdwlem6  15903  vdwlem9  15906  ramub1lem2  15944  cshwshashlem2  16011  qusaddvallem  16412  xpsaddlem  16436  xpsvsca  16440  mrcun  16483  homfeqval  16557  comfeqval  16568  sectcan  16615  sectco  16616  sectmon  16642  monsect  16643  funcsect  16732  setcmon  16937  resscatc  16955  catciso  16957  evlfcllem  17062  curf2cl  17072  curfcl  17073  yonedalem4c  17118  yonedalem3b  17120  yonedainv  17122  latj12  17297  mnd12g  17507  resmhm  17560  pwsco2mhm  17572  frmdup3lem  17604  grprcan  17656  grplcan  17678  grpasscan1  17679  grpinv11  17685  grpinvnz  17687  grplmulf1o  17690  grpinvpropd  17691  grpinvadd  17694  grpsubsub4  17709  dfgrp3  17715  imasgrp2  17731  mhmid  17737  mhmmnd  17738  mulgz  17768  mulgdirlem  17771  mulgdir  17772  mulgass  17777  mulgsubdir  17780  mulgpropd  17782  pwsmulg  17785  isnsg3  17826  nmzsubg  17833  ssnmz  17834  eqger  17842  eqglact  17843  ghminv  17865  conjnmz  17892  subgga  17930  gasubg  17932  galcan  17934  gacan  17935  cntzsubg  17966  cntzmhm  17968  psgnunilem2  18112  sylow1lem1  18210  sylow2blem2  18233  sylow2blem3  18234  lsmmod  18285  lsmpropd  18287  lsmdisj2  18292  subgdisj1  18301  subgdisj2  18302  efgredleme  18353  efgredlemd  18354  efgredlemc  18355  efgredlem  18357  frgpup3lem  18387  mulgdi  18429  ghmcmn  18434  lsm4  18460  cygabl  18489  gsummhm2  18536  gsumpt  18558  gsum2d  18568  dprdfeq0  18619  ablfac1eu  18670  ringcom  18777  isringd  18783  ringlz  18785  ringrz  18786  ring1eq0  18788  ringmneg1  18794  gsumdixp  18807  unitgrp  18865  irredrmul  18905  drngmul0or  18968  subrginv  18996  subrgunit  18998  abvrec  19036  srngnvl  19056  srngadd  19057  srngmul  19058  issrngd  19061  lmodvs0  19097  lmodvneg1  19106  lmodcom  19109  lmodsubdi  19120  lmodvsinv  19239  lmodvsinv2  19240  lmhmvsca  19248  lvecvs0or  19311  lvecinv  19316  lspsnvs  19317  lspabs2  19323  lspfixed  19331  lspfixedOLD  19332  lspsolv  19347  unitrrg  19498  asclpropd  19551  psrass1lem  19582  psrlidm  19608  psrridm  19609  mvrf1  19630  mplmon2mul  19705  evlslem1  19719  evlseu  19720  evlssca  19726  evlsvar  19727  coe1pwmul  19853  pf1ind  19923  prmirredlem  20045  mulgrhm2  20051  chrrhm  20083  znidomb  20113  psgnghm  20129  psgninv  20131  zrhpsgnodpm  20141  evpmodpmf1o  20146  psgndiflemB  20150  ip0r  20188  ipdir  20190  ipdi  20191  ipass  20196  ipassr  20197  phlpropd  20206  ocvpj  20267  uvcresum  20338  lmimlbs  20381  gsumcom3  20411  mat0dimbas0  20479  mdetrlin  20615  mdetrsca  20616  mdetr0  20618  mdetunilem8  20632  mdetuni0  20634  mdetmul  20636  maducoeval2  20653  madurid  20657  madulid  20658  matinv  20691  matunit  20692  slesolinv  20694  slesolinvbi  20695  cpmadugsumlemF  20890  restin  21180  cncmp  21405  cmpsublem  21412  conndisj  21429  cnconn  21435  kgencmp2  21559  ufldom  21975  tgplacthmeo  22116  ghmcnp  22127  qustgpopn  22132  qustgphaus  22135  tsmsxplem2  22166  tususp  22285  xpsdsval  22395  blpnfctr  22450  xmssym  22479  ressxms  22539  isngp2  22610  ngppropd  22650  nminvr  22682  blcvx  22810  icccvx  22958  pcohtpylem  23027  pcohtpy  23028  clmvscom  23098  cvsmuleqdivd  23142  cvsdiveqd  23143  pjthlem1  23416  ovollb2lem  23465  ovolicc2lem1  23494  ovolicc2lem5  23498  volsup  23533  ovolioo  23545  uniiccdif  23555  uniioombllem3  23562  uniioombllem4  23563  vitalilem3  23587  itg1sub  23686  itg2const  23717  iblcnlem1  23764  itgcnlem  23766  itgaddlem2  23800  itgsub  23802  itgabs  23811  ditgsplit  23835  dvmulbr  23912  dvcmul  23917  dvcmulf  23918  dvrec  23928  dvmptres3  23929  dvmptadd  23933  dvmptmul  23934  dvmptres2  23935  dvmptneg  23939  dvmptsub  23940  dvmptcj  23941  dvmptco  23945  dveflem  23952  dvlip  23966  dvlipcn  23967  dvlip2  23968  dvcvx  23993  dvfsumle  23994  dvfsumabs  23996  dvfsumlem1  23999  dvfsumlem2  24000  ftc2  24017  ftc2ditglem  24018  itgparts  24020  itgsubstlem  24021  itgsubst  24022  fta1glem1  24135  fta1blem  24138  plyeq0lem  24176  plymullem1  24180  coeeulem  24190  coe0  24222  coesub  24223  dvply1  24249  plydivlem4  24261  plyrem  24270  fta1lem  24272  vieta1  24277  plyexmo  24278  elqaalem2  24285  aareccl  24291  aannenlem1  24293  aaliou3lem2  24308  dvtaylp  24334  taylthlem1  24337  radcnvlem1  24377  pserdvlem2  24392  efcvx  24413  ptolemy  24459  tangtx  24468  efif1olem3  24501  efif1olem4  24502  efabl  24507  lognegb  24546  efiarg  24563  cosargd  24564  tanarg  24575  logtayl  24616  cxpneg  24637  cxpsub  24638  cxprec  24642  cxproot  24646  cxpsqrt  24659  cxpcn3lem  24698  cxpaddlelem  24702  abscxpbnd  24704  root1eq1  24706  cxpeq  24708  logrec  24711  isosctrlem2  24759  isosctrlem3  24760  isosctr  24761  ssscongptld  24762  chordthmlem  24769  heron  24775  quad2  24776  dcubic1lem  24780  mcubic  24784  cubic2  24785  cubic  24786  dquartlem2  24789  dquart  24790  quart1lem  24792  quart1  24793  asinlem2  24806  asinlem3  24808  asinsin  24829  sinacos  24842  atanlogsublem  24852  efiatan2  24854  2efiatan  24855  tanatan  24856  atantan  24860  atans2  24868  dvatan  24872  atantayl  24874  atantayl2  24875  log2cnv  24881  rlimcnp2  24903  cxplim  24908  cxp2lim  24913  cvxcl  24921  scvxcvx  24922  zetacvg  24951  lgamgulmlem4  24968  lgamcvg2  24991  gamp1  24994  wilthlem1  25004  wilthlem2  25005  ftalem5  25013  basellem3  25019  basellem5  25021  basellem8  25024  mumullem2  25116  musum  25127  musumsum  25128  muinv  25129  sgmppw  25132  1sgmprm  25134  1sgm2ppw  25135  ppiub  25139  logfac2  25152  chpchtsum  25154  perfectlem1  25164  perfectlem2  25165  dchrn0  25185  dchrfi  25190  dchrabs  25195  dchrptlem1  25199  dchrhash  25206  dchr2sum  25208  sum2dchr  25209  bposlem6  25224  bposlem9  25227  lgsvalmod  25251  lgsdilem  25259  lgsne0  25270  lgssq  25272  lgssq2  25273  lgsqr  25286  lgsdchrval  25289  lgsdchr  25290  gausslemma2dlem6  25307  gausslemma2d  25309  lgseisenlem1  25310  lgseisenlem2  25311  lgseisenlem4  25313  lgsquadlem1  25315  lgsquadlem3  25317  lgsquad3  25322  m1lgs  25323  rplogsumlem1  25383  rplogsumlem2  25384  dchrisumlem2  25389  dchrisum0fno1  25410  rpvmasum2  25411  dchrisum0lem1  25415  dchrisum0lem2  25417  mudivsum  25429  mulog2sumlem1  25433  vmalogdivsum  25438  2vmadivsumlem  25439  logsqvma  25441  selberglem2  25445  selberg2lem  25449  selberg3lem1  25456  selberg4lem1  25459  selberg4  25460  pntrsumo1  25464  selbergr  25467  selberg34r  25470  pntrlog2bndlem3  25478  pntrlog2bndlem4  25479  pntibndlem2  25490  pntlemg  25497  pntlemr  25501  pntlemf  25504  ostthlem1  25526  padicabvcxp  25531  ostth3  25537  tgcgrcomlr  25585  tgifscgr  25613  iscgrglt  25619  tgbtwnconn1lem2  25678  tgbtwnconn1lem3  25679  mirne  25772  miduniq2  25792  krippenlem  25795  ragcgr  25812  cgrg3col4  25944  f1otrg  25961  ttgcontlem1  25975  brbtwn2  25995  axsegconlem10  26016  ax5seglem3  26021  ax5seglem6  26024  axpaschlem  26030  axeuclidlem  26052  axcontlem2  26055  axcontlem7  26060  axcontlem8  26061  cusgrsizeindslem  26571  frgrncvvdeq  27480  numclwwlk7  27575  grpoidinvlem1  27683  grpoideu  27688  grporcan  27697  grpolcan  27709  grpoinvop  27712  ablo4  27729  nvscom  27808  nvmul0or  27829  nvz0  27847  smcnlem  27876  ipidsq  27889  sspz  27914  lno0  27935  lnoadd  27937  lnomul  27939  ipasslem3  28012  dipdi  28022  dipassr  28025  dipsubdi  28028  ubthlem2  28051  hvmul0or  28206  hvadd12  28216  hvadd4  28217  hvmulcom  28224  normneg  28325  pjhthlem1  28574  chj12  28717  spanunsni  28762  5oalem2  28838  3oalem2  28846  hoadd4  28967  homul12  28988  hosubdi  28991  honegsubdi  28993  hosub4  28996  adj2  29117  lnopmul  29150  lnopaddi  29154  lnfnaddi  29226  lnfnmuli  29227  cnlnadjlem6  29255  adjeq0  29274  leopmul  29317  opsqrlem1  29323  opsqrlem6  29328  hstnmoc  29406  strlem1  29433  chirredlem3  29575  fpwrelmapffslem  29830  subeqxfrd  29834  xaddeq0  29841  bcm1n  29877  divnumden2  29887  xmulcand  29950  xreceu  29951  bhmafibid1  29965  2sqmod  29969  xrsmulgzz  29999  xrge0adddir  30013  xrge0adddi  30014  abliso  30017  ogrpaddltrbid  30042  ogrpinvlt  30045  archiabllem1a  30066  archiabllem1  30068  archiabllem2c  30070  slmdvs0  30099  dvrcan5  30114  ornglmullt  30128  orngrmullt  30129  rhmunitinv  30143  mdetpmtr2  30211  madjusmdetlem1  30214  mdetlap  30219  qtophaus  30224  qqhval2lem  30346  esumpad  30438  esummulc1  30464  esumsup  30472  measxun2  30594  measssd  30599  inelcarsg  30694  carsggect  30701  carsgclctunlem2  30702  pmeasmono  30707  oddpwdc  30737  eulerpartlemgs2  30763  eulerpartlemn  30764  totprobd  30809  signstfvn  30967  signstfveq0  30975  ftc2re  30997  itgexpif  31005  breprexpnat  31033  circlemethnat  31040  circlevma  31041  circlemethhgt  31042  hgt750lemf  31052  hgt750lemg  31053  hgt750lemb  31055  tgoldbachgt  31062  bnj1379  31219  bnj1321  31413  subfaclim  31488  cvxsconn  31543  resconn  31546  cvmliftmolem1  31581  cvmliftlem7  31591  cvmliftlem13  31596  cvmlift2lem7  31609  cvmlift3lem5  31623  elmsta  31763  msubff1  31771  mthmpps  31797  bcm1nt  31940  faclim2  31951  funsseq  31983  nolesgn2o  32140  nolesgn2ores  32141  nodenselem5  32154  nolt02o  32161  noprefixmo  32164  clsun  32639  topjoin  32676  bj-bary1lem  33472  finxpreclem4  33542  matunitlindflem1  33713  ptrest  33716  poimirlem4  33721  poimirlem6  33723  poimirlem7  33724  poimirlem9  33726  poimirlem11  33728  poimirlem12  33729  poimirlem26  33743  poimirlem27  33744  itg2addnclem  33768  itg2addnclem3  33770  itgaddnclem2  33776  itgsubnc  33779  iblmulc2nc  33782  itgabsnc  33786  ftc2nc  33801  areacirclem1  33807  areacirclem4  33810  areacirc  33812  cocanfo  33819  ablo4pnp  33985  rngolz  34027  rngorz  34028  zerdivemp1x  34052  crngm4  34108  crngohomfo  34111  lfl0  34840  lfladd  34841  lflmul  34843  eqlkr3  34876  olm11  35002  latm12  35005  cmtcomlemN  35023  omlspjN  35036  hlatj12  35146  1cvrjat  35250  dalemrotyz  35433  padd12N  35614  pmapjlln1  35630  atmod2i1  35636  pmapocjN  35705  pnonsingN  35708  pexmidN  35744  lhp2at0  35807  lhpelim  35812  ltrncnv  35921  cdleme7c  36020  cdleme15b  36050  cdlemednpq  36074  cdleme20m  36098  cdleme22cN  36117  cdleme22d  36118  cdleme23b  36125  cdleme30a  36153  cdleme35h  36231  cdlemeg46frv  36300  cdlemg2fv2  36375  cdlemg2l  36378  cdlemg2m  36379  cdlemg8c  36404  cdlemg10bALTN  36411  cdlemg12  36425  cdlemg13a  36426  cdlemg18c  36455  cdlemg19  36459  trlcoat  36498  cdlemg47  36511  tendo1ne0  36603  cdlemk9  36614  cdlemk9bN  36615  dia2dimlem1  36839  tendolinv  36880  tendorinv  36881  dvhlveclem  36883  doca3N  36902  dihmeetlem7N  37085  dihjatc1  37086  dihmeetlem18N  37099  dochnoncon  37166  dihjatc  37192  dihjatcclem1  37193  dihjatcclem4  37196  dochsnkr  37247  lcfl7lem  37274  lcfl8  37277  lcfl9a  37280  lclkrlem1  37281  lclkrlem2e  37286  lclkrlem2j  37291  lcfrlem1  37317  lcfrlem9  37325  lcfrlem23  37340  lcfrlem31  37348  mapd0  37440  mapdpglem21  37467  baerlem3lem1  37482  baerlem5alem1  37483  mapdindp4  37498  mapdh6gN  37517  hdmap1l6g  37591  hgmapval0  37667  hgmaprnlem1N  37671  hlhilhillem  37735  diophrw  37818  eldioph2lem1  37819  pellexlem2  37890  pellexlem6  37894  pellex  37895  pell1234qrne0  37913  pell1234qrreccl  37914  pell1qrgaplem  37933  rmxm1  37994  oddcomabszz  38004  jm2.19lem1  38051  jm3.1lem2  38080  dnnumch3  38112  pwssplit4  38154  flcidc  38239  deg1mhm  38280  itgpowd  38294  radcnvrat  39007  nzprmdif  39012  hashnzfz  39013  dvsconst  39023  dvsid  39024  expgrowth  39028  bccm1k  39035  bccn1  39037  binomcxplemnotnn0  39049  subadd4b  39970  uzinico2  40263  sumnnodd  40336  limsupresuz  40409  limsupequzlem  40428  liminfresre  40485  liminfresuz  40490  climliminflimsupd  40507  icccncfext  40574  dvresntr  40606  itgsinexplem1  40643  itgsinexp  40644  stoweidlem1  40691  wallispi2lem2  40762  stirlinglem3  40766  stirlinglem5  40768  stirlinglem10  40773  stirlinglem15  40778  dirkertrigeqlem3  40790  dirkercncflem2  40794  fourierdlem26  40823  fourierdlem42  40839  fourierdlem66  40862  fourierdlem73  40869  fourierdlem81  40877  fourierdlem83  40879  fourierdlem107  40903  etransclem23  40947  meaiininclem  41176  vonvolmbl  41351  iccvonmbllem  41368  sigaradd  41531  cevathlem1  41532  imarnf1pr  41866  m1mod0mod1  41908  fmtnorec3  42029  proththd  42100  perfectALTVlem1  42199  perfectALTVlem2  42200  rnglz  42446  pw2m1lepw2m1  42872  nnpw2pmod  42939  dignn0flhalflem1  42971  aacllem  43112  amgmlemALT  43114  young2d  43116
  Copyright terms: Public domain W3C validator