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

Theorem 3eqtr3d 2504
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  |-  ( ph  ->  A  =  B )
3eqtr3d.2  |-  ( ph  ->  A  =  C )
3eqtr3d.3  |-  ( ph  ->  B  =  D )
Assertion
Ref Expression
3eqtr3d  |-  ( ph  ->  C  =  D )

Proof of Theorem 3eqtr3d
StepHypRef Expression
1 3eqtr3d.1 . . 3  |-  ( ph  ->  A  =  B )
2 3eqtr3d.2 . . 3  |-  ( ph  ->  A  =  C )
31, 2eqtr3d 2498 . 2  |-  ( ph  ->  B  =  C )
4 3eqtr3d.3 . 2  |-  ( ph  ->  B  =  D )
53, 4eqtr3d 2498 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1455
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-cleq 2455
This theorem is referenced by:  mpteqb  5987  fvmptt  5988  fsnunfv  6128  f1ocnvfv1  6200  f1ocnvfv2  6201  fcof1  6210  weniso  6270  caov12d  6517  caov13d  6519  caov411d  6521  caovmo  6533  grprinvlem  6534  grprinvd  6535  grpridd  6536  onovuni  7087  tfrlem5  7124  seqomlem1  7193  seqomlem4  7196  onasuc  7256  onesuc  7258  oeeui  7329  fopwdom  7706  unxpdomlem2  7803  cantnfres  8208  cnfcom2lem  8232  cnfcom2  8233  cardiun  8442  ackbij1lem16  8691  ackbij2lem2  8696  fpwwe2lem6  9086  fpwwe2lem8  9088  canthp1lem2  9104  mul12  9825  mul4  9828  addid1  9839  addcan  9843  addcom  9845  addcomd  9861  add12  9872  ppncan  9942  addsub4  9943  muladd  10079  mulcand  10273  receu  10285  div13  10319  divdivdiv  10336  divcan5  10337  divdiv1  10346  divdiv2  10347  halfaddsub  10875  xadddi  11610  xov1plusxeqvd  11807  fztp  11881  flzadd  12091  fldiv  12119  modnegd  12177  modsub12d  12179  2submod  12183  seqm1  12262  seqcaopr  12282  seqf1o  12286  exprec  12345  expsub  12352  zesq  12427  digit1  12438  discr1  12440  discr  12441  facnn2  12500  faclbnd6  12516  hashfz1  12561  hashdom  12590  hashun  12593  hashbclem  12648  hashfac  12654  seqcoll  12660  ccatopth  12863  repsw2  13074  repsw3  13075  shftval3  13188  crre  13226  resub  13239  imsub  13247  cjsub  13261  abslem2  13451  sqreulem  13471  climshft2  13695  isercolllem2  13778  iseraltlem2  13798  iseraltlem3  13799  fsumsub  13898  telfsumo  13911  telfsumo2  13912  hashiun  13931  bcxmas  13942  climcndslem1  13956  climcndslem2  13957  trireciplem  13969  geoser  13974  geo2sum2  13979  fprodm1  14070  fallfacfwd  14138  binomfallfaclem2  14142  bpolydiflem  14156  bpoly4  14161  fsumcube  14162  sinsub  14271  cossub  14272  rpnnen2lem10  14325  ruclem12  14342  divalglem9  14430  divalglem9OLD  14431  bitsinv1lem  14464  bitsinv1  14465  bitsf1  14469  sadasslem  14493  bitsres  14496  smup1  14512  smumul  14516  modgcd  14549  absmulgcd  14564  gcdmultiplez  14568  eucalg  14595  lcmgcd  14621  lcmid  14623  lcmftp  14658  numdensq  14752  dfphi2  14771  phiprm  14774  fermltl  14781  prmdiveq  14783  odzdvds  14789  odzdvdsOLD  14795  powm2modprm  14803  modprm0  14805  coprimeprodsq  14808  pythagtriplem6  14820  pythagtriplem7  14821  pythagtriplem12  14825  pythagtriplem16  14829  pcaddlem  14882  sumhash  14890  pcfac  14893  pockthlem  14898  prmreclem6  14914  4sqlem12  14949  4sqlem15OLD  14952  4sqlem15  14958  vdwlem3  14982  vdwlem6  14985  vdwlem9  14988  ramub1lem2  15034  cshwshashlem2  15116  qusaddvallem  15506  xpsaddlem  15530  xpsvsca  15534  mrcun  15577  homfeqval  15651  comfeqval  15662  sectcan  15709  sectco  15710  sectmon  15736  monsect  15737  funcsect  15826  setcmon  16031  resscatc  16049  catciso  16051  evlfcllem  16155  curf2cl  16165  curfcl  16166  yonedalem4c  16211  yonedalem3b  16213  yonedainv  16215  latj12  16391  mnd12g  16601  resmhm  16655  pwsco2mhm  16667  frmdup3lem  16699  grprcan  16748  grplcan  16767  grpinv11  16772  grpinvnz  16774  grplmulf1o  16777  grpinvpropd  16778  grpinvadd  16781  grpsubsub4  16796  mulgz  16828  mulgdirlem  16831  mulgdir  16832  mulgass  16837  mulgsubdir  16838  mulgpropd  16840  pwsmulg  16849  imasgrp2  16850  mhmid  16856  mhmmnd  16857  isnsg3  16900  nmzsubg  16907  ssnmz  16908  eqger  16916  eqglact  16917  ghminv  16939  conjnmz  16965  subgga  17003  gasubg  17005  galcan  17007  gacan  17008  cntzsubg  17039  cntzmhm  17041  psgnunilem2  17185  sylow1lem1  17299  sylow2blem2  17322  sylow2blem3  17323  lsmmod  17374  lsmpropd  17376  lsmdisj2  17381  subgdisj1  17390  subgdisj2  17391  efgredleme  17442  efgredlemd  17443  efgredlemc  17444  efgredlem  17446  frgpup3lem  17476  mulgdi  17516  ghmcmn  17521  lsm4  17547  cygabl  17574  gsummhm2  17621  gsumpt  17643  gsum2d  17653  dprdfeq0  17704  ablfac1eu  17755  ringcom  17858  isringd  17864  ringlz  17866  ringrz  17867  ring1eq0  17869  ringmneg1  17873  gsumdixp  17886  unitgrp  17944  irredrmul  17984  drngmul0or  18045  subrginv  18073  subrgunit  18075  abvrec  18113  srngnvl  18133  srngadd  18134  srngmul  18135  issrngd  18138  lmodvs0  18174  lmodvneg1  18180  lmodcom  18183  lmodsubdi  18194  lmodvsinv  18308  lmodvsinv2  18309  lmhmvsca  18317  lvecvs0or  18380  lvecinv  18385  lspsnvs  18386  lspabs2  18392  lspfixed  18400  lspsolv  18415  unitrrg  18566  asclpropd  18619  psrass1lem  18650  psrlidm  18676  psrridm  18677  mvrf1  18698  mplmon2mul  18773  evlslem1  18787  evlseu  18788  evlssca  18794  evlsvar  18795  coe1pwmul  18921  pf1ind  18992  prmirredlem  19113  mulgrhm2  19119  chrrhm  19151  znidomb  19181  psgnghm  19197  psgninv  19199  zrhpsgnodpm  19209  evpmodpmf1o  19213  psgndiflemB  19217  ip0r  19253  ipdir  19255  ipdi  19256  ipass  19261  ipassr  19262  phlpropd  19271  ocvpj  19329  uvcresum  19400  lmimlbs  19443  gsumcom3  19473  mat0dimbas0  19540  mdetrlin  19676  mdetrsca  19677  mdetr0  19679  mdetunilem8  19693  mdetuni0  19695  mdetmul  19697  maducoeval2  19714  madurid  19718  madulid  19719  matinv  19751  matunit  19752  slesolinv  19754  slesolinvbi  19755  cpmadugsumlemF  19949  restin  20231  cncmp  20456  cmpsublem  20463  conndisj  20480  cnconn  20486  kgencmp2  20610  ufldom  21026  tgplacthmeo  21167  ghmcnp  21178  qustgpopn  21183  qustgphaus  21186  tsmsxplem2  21217  tususp  21336  xpsdsval  21445  blpnfctr  21500  xmssym  21529  ressxms  21589  isngp2  21660  ngppropd  21694  nminvr  21721  blcvx  21865  icccvx  22027  pcohtpylem  22099  pcohtpy  22100  cvsmuleqdivd  22191  cvsdiveqd  22192  pjthlem1  22440  ovollb2lem  22490  ovolicc2lem1  22519  ovolicc2lem5  22524  volsup  22558  ovolioo  22570  uniiccdif  22584  uniioombllem3  22592  uniioombllem4  22593  vitalilem3  22617  itg1sub  22716  itg2const  22747  iblcnlem1  22794  itgcnlem  22796  itgaddlem2  22830  itgsub  22832  itgabs  22841  ditgsplit  22865  dvmulbr  22942  dvcmul  22947  dvcmulf  22948  dvrec  22958  dvmptres3  22959  dvmptadd  22963  dvmptmul  22964  dvmptres2  22965  dvmptneg  22969  dvmptsub  22970  dvmptcj  22971  dvmptco  22975  dveflem  22980  dvlip  22994  dvlipcn  22995  dvlip2  22996  dvcvx  23021  dvfsumle  23022  dvfsumabs  23024  dvfsumlem1  23027  dvfsumlem2  23028  ftc2  23045  ftc2ditglem  23046  itgparts  23048  itgsubstlem  23049  itgsubst  23050  fta1glem1  23165  fta1blem  23168  plyeq0lem  23213  plymullem1  23217  coeeulem  23227  coe0  23259  coesub  23260  dvply1  23286  plydivlem4  23298  plyrem  23307  fta1lem  23309  vieta1  23314  plyexmo  23315  elqaalem2  23322  elqaalem2OLD  23325  aareccl  23331  aannenlem1  23333  aaliou3lem2  23348  dvtaylp  23374  taylthlem1  23377  radcnvlem1  23417  pserdvlem2  23432  efcvx  23453  ptolemy  23500  tangtx  23509  efif1olem3  23542  efif1olem4  23543  efabl  23548  lognegb  23588  efiarg  23605  cosargd  23606  tanarg  23617  logtayl  23654  cxpneg  23675  cxpsub  23676  cxprec  23680  cxproot  23684  cxpsqrt  23697  cxpcn3lem  23736  cxpaddlelem  23740  abscxpbnd  23742  root1eq1  23744  cxpeq  23746  logrec  23749  isosctrlem2  23797  isosctrlem3  23798  isosctr  23799  ssscongptld  23800  chordthmlem  23807  heron  23813  quad2  23814  dcubic1lem  23818  mcubic  23822  cubic2  23823  cubic  23824  dquartlem2  23827  dquart  23828  quart1lem  23830  quart1  23831  asinlem2  23844  asinlem3  23846  asinsin  23867  sinacos  23880  atanlogsublem  23890  efiatan2  23892  2efiatan  23893  tanatan  23894  atantan  23898  atans2  23906  dvatan  23910  atantayl  23912  atantayl2  23913  log2cnv  23919  rlimcnp2  23941  cxplim  23946  cxp2lim  23951  cvxcl  23959  scvxcvx  23960  zetacvg  23989  lgamgulmlem4  24006  lgamcvg2  24029  gamp1  24032  wilthlem1  24042  wilthlem2  24043  ftalem5  24050  ftalem5OLD  24052  basellem3  24058  basellem5  24060  basellem8  24063  mumullem2  24156  musum  24169  musumsum  24170  muinv  24171  sgmppw  24174  1sgmprm  24176  1sgm2ppw  24177  ppiub  24181  logfac2  24194  chpchtsum  24196  perfectlem1  24206  perfectlem2  24207  dchrn0  24227  dchrfi  24232  dchrabs  24237  dchrptlem1  24241  dchrhash  24248  dchr2sum  24250  sum2dchr  24251  bposlem6  24266  bposlem9  24269  lgsvalmod  24292  lgsdilem  24299  lgsne0  24310  lgssq  24312  lgssq2  24313  lgsqr  24323  lgsdchrval  24324  lgsdchr  24325  lgseisenlem1  24326  lgseisenlem2  24327  lgseisenlem4  24329  lgsquadlem1  24331  lgsquadlem3  24333  lgsquad3  24338  m1lgs  24339  rplogsumlem1  24371  rplogsumlem2  24372  dchrisumlem2  24377  dchrisum0fno1  24398  rpvmasum2  24399  dchrisum0lem1  24403  dchrisum0lem2  24405  mudivsum  24417  mulog2sumlem1  24421  vmalogdivsum  24426  2vmadivsumlem  24427  logsqvma  24429  selberglem2  24433  selberg2lem  24437  selberg3lem1  24444  selberg4lem1  24447  selberg4  24448  pntrsumo1  24452  selbergr  24455  selberg34r  24458  pntrlog2bndlem3  24466  pntrlog2bndlem4  24467  pntibndlem2  24478  pntlemg  24485  pntlemr  24489  pntlemf  24492  ostthlem1  24514  padicabvcxp  24519  ostth3  24525  tgcgrcomlr  24573  tgifscgr  24602  iscgrglt  24608  tgbtwnconn1lem2  24667  tgbtwnconn1lem3  24668  mirne  24761  miduniq2  24781  krippenlem  24784  ragcgr  24801  cgrg3col4  24933  f1otrg  24950  ttgcontlem1  24964  brbtwn2  24984  axsegconlem10  25005  ax5seglem3  25010  ax5seglem6  25013  axpaschlem  25019  axeuclidlem  25041  axcontlem2  25044  axcontlem7  25049  axcontlem8  25050  cusgrasizeindslem3  25252  frgrancvvdeq  25819  frgrancvvdgeq  25820  numclwwlk7  25891  grpoidinvlem1  25981  grpoideu  25986  grporcan  25998  grpolcan  26010  grpoasscan1  26014  grpoinvop  26018  grpopnpcan2  26030  gxsuc  26049  gxsub  26053  gxmul  26055  ablo4  26064  subgoinv  26085  ablomul  26132  ghgrpOLD  26145  ghabloOLD  26146  rngolz  26178  rngorz  26179  zerdivemp1  26211  nvadd12  26291  nvscom  26299  nvmul0or  26322  nvz0  26346  smcnlem  26382  ipidsq  26398  sspz  26423  lno0  26446  lnoadd  26448  lnomul  26450  ipasslem3  26523  dipdi  26533  dipassr  26536  dipsubdi  26539  ubthlem2  26562  hvmul0or  26727  hvadd12  26737  hvadd4  26738  hvmulcom  26745  normneg  26846  pjhthlem1  27093  chj12  27236  spanunsni  27281  5oalem2  27357  3oalem2  27365  hoadd4  27486  homul12  27507  hosubdi  27510  honegsubdi  27512  hosub4  27515  adj2  27636  lnopmul  27669  lnopaddi  27673  lnfnaddi  27745  lnfnmuli  27746  cnlnadjlem6  27774  adjeq0  27793  leopmul  27836  opsqrlem1  27842  opsqrlem6  27847  hstnmoc  27925  strlem1  27952  chirredlem3  28094  fpwrelmapffslem  28366  subeqxfrd  28370  addeqxfrd  28371  xaddeq0  28379  bcm1n  28420  divnumden2  28430  xmulcand  28439  xreceu  28440  bhmafibid1  28454  2sqmod  28458  xrsmulgzz  28489  xrge0adddir  28504  xrge0adddi  28505  abliso  28508  ogrpaddltrbid  28533  ogrpinvlt  28536  archiabllem1a  28557  archiabllem1  28559  archiabllem2c  28561  slmdvs0  28590  dvrcan5  28605  ornglmullt  28619  orngrmullt  28620  rhmunitinv  28634  mdetpmtr2  28699  madjusmdetlem1  28702  mdetlap  28707  qtophaus  28712  qqhval2lem  28834  esumpad  28925  esummulc1  28951  esumsup  28959  measxun2  29081  measssd  29086  inelcarsg  29192  carsggect  29199  carsgclctunlem2  29200  pmeasmono  29206  oddpwdc  29236  eulerpartlemgs2  29262  eulerpartlemn  29263  totprobd  29308  signstfvn  29507  signstfveq0  29515  bnj1379  29691  bnj1321  29885  subfaclim  29960  cvxscon  30015  rescon  30018  cvmliftmolem1  30053  cvmliftlem7  30063  cvmliftlem13  30068  cvmlift2lem7  30081  cvmlift3lem5  30095  elmsta  30235  msubff1  30243  mthmpps  30269  ghomf1olem  30361  bcm1nt  30422  faclim2  30433  funsseq  30458  clsun  31033  topjoin  31070  bj-bary1lem  31760  finxpreclem4  31831  ptrest  31984  poimirlem4  31989  poimirlem6  31991  poimirlem7  31992  poimirlem9  31994  poimirlem11  31996  poimirlem12  31997  poimirlem26  32011  poimirlem27  32012  itg2addnclem  32038  itg2addnclem3  32040  itgaddnclem2  32046  itgsubnc  32049  iblmulc2nc  32052  itgabsnc  32056  ftc2nc  32071  areacirclem1  32077  areacirclem4  32080  areacirc  32082  cocanfo  32089  ablo4pnp  32223  zerdivemp1x  32239  crngm4  32281  crngohomfo  32284  fsumshftdOLD  32569  lfl0  32676  lfladd  32677  lflmul  32679  eqlkr3  32712  olm11  32838  latm12  32841  cmtcomlemN  32859  omlspjN  32872  hlatj12  32981  1cvrjat  33085  dalemrotyz  33268  padd12N  33449  pmapjlln1  33465  atmod2i1  33471  pmapocjN  33540  pnonsingN  33543  pexmidN  33579  lhp2at0  33642  lhpelim  33647  ltrncnv  33756  ltrnmwOLD  33762  cdleme7c  33856  cdleme15b  33886  cdlemednpq  33910  cdleme20yOLD  33914  cdleme20m  33935  cdleme22cN  33954  cdleme22d  33955  cdleme23b  33962  cdleme30a  33990  cdleme35h  34068  cdlemeg46frv  34137  cdlemg2fv2  34212  cdlemg2l  34215  cdlemg2m  34216  cdlemg8c  34241  cdlemg10bALTN  34248  cdlemg12  34262  cdlemg13a  34263  cdlemg18c  34292  cdlemg19  34296  trlcoat  34335  cdlemg47  34348  tendo1ne0  34440  cdlemk9  34451  cdlemk9bN  34452  dia2dimlem1  34677  tendolinv  34718  tendorinv  34719  dvhlveclem  34721  doca3N  34740  dihmeetlem7N  34923  dihjatc1  34924  dihmeetlem18N  34937  dochnoncon  35004  dihjatc  35030  dihjatcclem1  35031  dihjatcclem4  35034  dochsnkr  35085  lcfl7lem  35112  lcfl8  35115  lcfl9a  35118  lclkrlem1  35119  lclkrlem2e  35124  lclkrlem2j  35129  lcfrlem1  35155  lcfrlem9  35163  lcfrlem23  35178  lcfrlem31  35186  mapd0  35278  mapdpglem21  35305  baerlem3lem1  35320  baerlem5alem1  35321  mapdindp4  35336  mapdh6gN  35355  hdmap1l6g  35430  hgmapval0  35508  hgmaprnlem1N  35512  hlhilhillem  35576  diophrw  35646  eldioph2lem1  35647  pellexlem2  35719  pellexlem6  35723  pellex  35724  pell1234qrne0  35744  pell1234qrreccl  35745  pell1qrgaplem  35764  rmxm1  35827  oddcomabszz  35837  jm2.19lem1  35889  jm3.1lem2  35918  dnnumch3  35950  pwssplit4  35992  flcidc  36085  hashgcdlem  36119  deg1mhm  36129  itgpowd  36144  radcnvrat  36707  nzprmdif  36712  hashnzfz  36713  dvsconst  36723  dvsid  36724  expgrowth  36728  bccm1k  36735  bccn1  36737  binomcxplemnotnn0  36749  subadd4b  37530  sumnnodd  37748  icccncfext  37803  dvresntr  37826  itgsinexplem1  37868  itgsinexp  37869  stoweidlem1  37899  wallispi2lem2  37972  stirlinglem3  37976  stirlinglem5  37978  stirlinglem10  37983  stirlinglem15  37988  dirkertrigeqlem3  38000  dirkercncflem2  38004  fourierdlem26  38033  fourierdlem42  38050  fourierdlem42OLD  38051  fourierdlem66  38074  fourierdlem73  38081  fourierdlem81  38089  fourierdlem83  38091  fourierdlem107  38115  etransclem23  38160  sigaradd  38513  cevathlem1  38514  m1mod0mod1  38761  mod2eq1n2dvds  38763  perfectALTVlem1  38881  perfectALTVlem2  38882  proththd  38952  imarnf1pr  39058  cusgrsizeindslem  39562  usgrauvtxvd  39945  rnglz  40157  pw2m1lepw2m1  40591  nnpw2pmod  40667  dignn0flhalflem1  40699  aacllem  40813
  Copyright terms: Public domain W3C validator