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

Theorem 3eqtr3d 2503
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 2497 . 2  |-  ( ph  ->  B  =  C )
4 3eqtr3d.3 . 2  |-  ( ph  ->  B  =  D )
53, 4eqtr3d 2497 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-cleq 2446
This theorem is referenced by:  mpteqb  5896  fvmptt  5897  fsnunfv  6026  f1ocnvfv1  6091  f1ocnvfv2  6092  fcof1  6099  weniso  6153  caov12d  6393  caov13d  6395  caov411d  6397  caovmo  6409  grprinvlem  6410  grprinvd  6411  grpridd  6412  onovuni  6912  tfrlem5  6948  seqomlem1  7014  seqomlem4  7017  onasuc  7077  onesuc  7079  oeeui  7150  fopwdom  7528  unxpdomlem2  7628  cantnfres  7995  cnfcom2lem  8044  cnfcom2  8045  cnfcom2lemOLD  8052  cnfcom2OLD  8053  cardiun  8262  ackbij1lem16  8514  ackbij2lem2  8519  fpwwe2lem6  8912  fpwwe2lem8  8914  canthp1lem2  8930  mul12  9645  mul4  9648  addid1  9659  addcan  9663  addcom  9665  addcomd  9681  add12  9692  ppncan  9761  addsub4  9762  muladd  9887  mulcand  10079  receu  10091  div13  10125  divdivdiv  10142  divcan5  10143  divdiv1  10152  divdiv2  10153  halfaddsub  10668  uzindOLD  10846  xadddi  11368  xov1plusxeqvd  11547  fztp  11628  flzadd  11787  fldiv  11815  addmodid  11864  modnegd  11870  modsub12d  11872  2submod  11876  seqm1  11939  seqcaopr  11959  seqf1o  11963  expsub  12027  zesq  12103  digit1  12114  discr1  12116  discr  12117  facnn2  12176  faclbnd6  12191  hashfz1  12233  hashdom  12259  hashun  12262  hashbclem  12322  hashfac  12328  seqcoll  12333  wrdlenccats1lenm1  12422  ccatopth  12481  repsw2  12667  repsw3  12668  shftval3  12682  crre  12720  resub  12733  imsub  12741  cjsub  12755  abslem2  12944  sqreulem  12964  climshft2  13177  isercolllem2  13260  iseraltlem2  13277  iseraltlem3  13278  fsumsub  13372  fsumtscopo  13382  fsumtscopo2  13383  hashiun  13402  bcxmas  13415  climcndslem1  13429  climcndslem2  13430  trireciplem  13441  geoser  13446  geo2sum2  13451  sinsub  13569  cossub  13570  rpnnen2lem10  13623  ruclem12  13640  divalglem9  13722  bitsinv1lem  13754  bitsinv1  13755  bitsf1  13759  sadasslem  13783  bitsres  13786  smup1  13802  smumul  13806  modgcd  13837  absmulgcd  13848  gcdmultiplez  13852  eucalg  13879  numdensq  13949  dfphi2  13966  phiprm  13969  fermltl  13976  prmdiveq  13978  odzdvds  13984  modprm0  13990  coprimeprodsq  13993  pythagtriplem6  14005  pythagtriplem7  14006  pythagtriplem12  14010  pythagtriplem16  14014  pcaddlem  14067  sumhash  14075  pcfac  14078  pockthlem  14083  prmreclem6  14099  4sqlem12  14134  4sqlem15  14137  vdwlem3  14161  vdwlem6  14164  vdwlem9  14167  ramub1lem2  14205  cshwshashlem2  14240  divsaddvallem  14607  xpsaddlem  14631  xpsvsca  14635  mrcun  14678  homfeqval  14754  comfeqval  14765  sectcan  14812  sectco  14813  sectmon  14834  monsect  14835  funcsect  14900  setcmon  15073  resscatc  15091  catciso  15093  evlfcllem  15149  curf2cl  15159  curfcl  15160  yonedalem4c  15205  yonedalem3b  15207  yonedainv  15209  latj12  15384  mnd12g  15543  resmhm  15605  pwsco2mhm  15617  frmdup3  15662  grprcan  15689  grplcan  15708  grpinv11  15713  grpinvnz  15715  grplmulf1o  15718  grpinvpropd  15719  grpinvadd  15722  grpsubsub4  15736  mulgz  15766  mulgdirlem  15769  mulgdir  15770  mulgass  15775  mulgsubdir  15776  mulgpropd  15778  pwsmulg  15787  imasgrp2  15788  isnsg3  15833  nmzsubg  15840  ssnmz  15841  eqger  15849  eqglact  15850  ghminv  15872  conjnmz  15898  subgga  15936  gasubg  15938  galcan  15940  gacan  15941  cntzsubg  15972  cntzmhm  15974  psgnunilem2  16119  sylow1lem1  16217  sylow2blem2  16240  sylow2blem3  16241  lsmmod  16292  lsmpropd  16294  lsmdisj2  16299  subgdisj1  16308  subgdisj2  16309  efgredleme  16360  efgredlemd  16361  efgredlemc  16362  efgredlem  16364  frgpup3lem  16394  mulgdi  16434  lsm4  16462  cygabl  16487  gsummhm2  16555  gsummhm2OLD  16556  gsumpt  16575  gsumptOLD  16576  gsum2d  16584  gsum2dOLD  16585  dprdfeq0  16633  dprdfeq0OLD  16640  ablfac1eu  16695  rngcom  16795  isrngd  16801  rnglz  16803  rngrz  16804  rng1eq0  16806  rngmneg1  16809  gsumdixpOLD  16822  gsumdixp  16823  unitgrp  16881  irredrmul  16921  drngmul0or  16975  subrginv  17003  subrgunit  17005  srngnvl  17063  srngadd  17064  srngmul  17065  issrngd  17068  lmodvs0  17104  lmodvneg1  17110  lmodcom  17113  lmodsubdi  17124  lmodvsinv  17239  lmodvsinv2  17240  lmhmvsca  17248  lvecvs0or  17311  lvecinv  17316  lspsnvs  17317  lspabs2  17323  lspfixed  17331  lspsolv  17346  unitrrg  17487  asclpropd  17538  psrass1lem  17569  psrlidm  17596  psrlidmOLD  17597  psrridm  17598  psrridmOLD  17599  mvrf1  17621  mplmon2mul  17706  evlslem1  17724  evlseu  17725  evlssca  17731  evlsvar  17732  coe1pwmul  17855  pf1ind  17913  prmirredlem  18041  prmirredlemOLD  18044  mulgrhm2  18051  mulgrhm2OLD  18054  chrrhm  18086  znidomb  18118  psgnghm  18134  psgninv  18136  zrhpsgnodpm  18146  evpmodpmf1o  18150  psgndiflemB  18154  ip0r  18190  ipdir  18192  ipdi  18193  ipass  18198  ipassr  18199  phlpropd  18208  ocvpj  18266  uvcresum  18342  lmimlbs  18389  gsumcom3  18423  mat0dimbas0  18449  mdetrlin  18539  mdetrsca  18540  mdetr0  18542  mdetunilem8  18556  mdetuni0  18558  mdetmul  18560  maducoeval2  18577  madurid  18581  madulid  18582  matinv  18614  matunit  18615  slesolinv  18617  slesolinvbi  18618  restin  18901  cncmp  19126  cmpsublem  19133  conndisj  19151  cnconn  19157  kgencmp2  19250  ufldom  19666  tgplacthmeo  19805  ghmcnp  19816  divstgpopn  19821  divstgphaus  19824  tsmsxplem2  19859  tususp  19978  xpsdsval  20087  blpnfctr  20142  xmssym  20171  ressxms  20231  isngp2  20320  ngppropd  20354  nminvr  20381  blcvx  20506  icccvx  20653  pcohtpylem  20722  pcohtpy  20723  cvsmuleqdivd  20814  cvsdiveqd  20815  pjthlem1  21055  ovollb2lem  21102  ovolicc2lem1  21131  ovolicc2lem5  21135  volsup  21169  ovolioo  21181  uniiccdif  21190  uniioombllem3  21197  uniioombllem4  21198  vitalilem3  21222  itg1sub  21319  itg2const  21350  iblcnlem1  21397  itgcnlem  21399  itgaddlem2  21433  itgsub  21435  itgabs  21444  ditgsplit  21468  dvmulbr  21545  dvcmul  21550  dvcmulf  21551  dvrec  21561  dvmptres3  21562  dvmptadd  21566  dvmptmul  21567  dvmptres2  21568  dvmptneg  21572  dvmptsub  21573  dvmptcj  21574  dvmptco  21578  dveflem  21583  dvlip  21597  dvlipcn  21598  dvlip2  21599  dvcvx  21624  dvfsumle  21625  dvfsumabs  21627  dvfsumlem1  21630  dvfsumlem2  21631  ftc2  21648  ftc2ditglem  21649  itgparts  21651  itgsubstlem  21652  itgsubst  21653  fta1glem1  21769  fta1blem  21772  plyeq0lem  21810  plymullem1  21814  coeeulem  21824  coe0  21855  coesub  21856  dvply1  21882  plydivlem4  21894  plyrem  21903  fta1lem  21905  vieta1  21910  plyexmo  21911  elqaalem2  21918  aareccl  21924  aannenlem1  21926  aaliou3lem2  21941  dvtaylp  21967  taylthlem1  21970  radcnvlem1  22010  pserdvlem2  22025  efcvx  22046  ptolemy  22090  tangtx  22099  efif1olem3  22132  efif1olem4  22133  lognegb  22170  efiarg  22188  cosargd  22189  tanarg  22200  logtayl  22237  cxpsub  22259  cxproot  22267  cxpsqr  22280  cxpcn3lem  22317  cxpaddlelem  22321  abscxpbnd  22323  root1eq1  22325  cxpeq  22327  logrec  22347  isosctrlem2  22349  isosctrlem3  22350  isosctr  22351  ssscongptld  22352  chordthmlem  22359  heron  22365  quad2  22366  dcubic1lem  22370  mcubic  22374  cubic2  22375  cubic  22376  dquartlem2  22379  dquart  22380  quart1lem  22382  quart1  22383  asinlem2  22396  asinlem3  22398  asinsin  22419  sinacos  22432  atanlogsublem  22442  efiatan2  22444  2efiatan  22445  tanatan  22446  atantan  22450  atans2  22458  dvatan  22462  atantayl  22464  atantayl2  22465  log2cnv  22471  rlimcnp2  22492  cxplim  22497  cxp2lim  22502  cvxcl  22510  scvxcvx  22511  wilthlem1  22538  wilthlem2  22539  ftalem5  22546  basellem3  22552  basellem5  22554  basellem8  22557  mumullem2  22650  musum  22663  musumsum  22664  muinv  22665  sgmppw  22668  1sgmprm  22670  1sgm2ppw  22671  ppiub  22675  logfac2  22688  chpchtsum  22690  perfectlem1  22700  perfectlem2  22701  dchrn0  22721  dchrfi  22726  dchrabs  22731  dchrptlem1  22735  dchrhash  22742  dchr2sum  22744  sum2dchr  22745  bposlem6  22760  bposlem9  22763  lgsvalmod  22786  lgsdilem  22793  lgsne0  22804  lgssq  22806  lgssq2  22807  lgsqr  22817  lgsdchrval  22818  lgsdchr  22819  lgseisenlem1  22820  lgseisenlem2  22821  lgseisenlem4  22823  lgsquadlem1  22825  lgsquadlem3  22827  lgsquad3  22832  m1lgs  22833  rplogsumlem1  22865  rplogsumlem2  22866  dchrisumlem2  22871  dchrisum0fno1  22892  rpvmasum2  22893  dchrisum0lem1  22897  dchrisum0lem2  22899  mudivsum  22911  mulog2sumlem1  22915  vmalogdivsum  22920  2vmadivsumlem  22921  logsqvma  22923  selberglem2  22927  selberg2lem  22931  selberg3lem1  22938  selberg4lem1  22941  selberg4  22942  pntrsumo1  22946  selbergr  22949  selberg34r  22952  pntrlog2bndlem3  22960  pntrlog2bndlem4  22961  pntibndlem2  22972  pntlemg  22979  pntlemr  22983  pntlemf  22986  ostthlem1  23008  padicabvcxp  23013  ostth3  23019  tgcgrcomlr  23067  tgbtwnconn1lem2  23141  tgbtwnconn1lem3  23142  krippenlem  23226  ragcgr  23243  f1otrg  23268  ttgcontlem1  23282  brbtwn2  23302  axsegconlem10  23323  ax5seglem3  23328  ax5seglem6  23331  axpaschlem  23337  axeuclidlem  23359  axcontlem2  23362  axcontlem7  23367  axcontlem8  23368  cusgrasizeindslem3  23534  grpoidinvlem1  23842  grpoideu  23847  grporcan  23859  grpolcan  23871  grpoasscan1  23875  grpoinvop  23879  grpopnpcan2  23891  gxsuc  23910  gxsub  23914  gxmul  23916  ablo4  23925  subgoinv  23946  ablomul  23993  ghgrp  24006  ghablo  24007  rngolz  24039  rngorz  24040  zerdivemp1  24072  nvadd12  24152  nvscom  24160  nvmul0or  24183  nvz0  24207  smcnlem  24243  ipidsq  24259  sspz  24284  lno0  24307  lnoadd  24309  lnomul  24311  ipasslem3  24384  dipdi  24394  dipassr  24397  dipsubdi  24400  ubthlem2  24423  hvmul0or  24578  hvadd12  24588  hvadd4  24589  hvmulcom  24596  normneg  24697  pjhthlem1  24945  chj12  25088  spanunsni  25133  5oalem2  25209  3oalem2  25217  mayete3iOLD  25283  hoadd4  25339  homul12  25360  hosubdi  25363  honegsubdi  25365  hosub4  25368  adj2  25489  lnopmul  25522  lnopaddi  25526  lnfnaddi  25598  lnfnmuli  25599  cnlnadjlem6  25627  adjeq0  25646  leopmul  25689  opsqrlem1  25695  opsqrlem6  25700  hstnmoc  25778  strlem1  25805  chirredlem3  25947  fpwrelmapffslem  26182  xaddeq0  26196  bcm1n  26223  divnumden2  26231  xmulcand  26240  xreceu  26241  xrsmulgzz  26283  xrge0adddir  26299  xrge0adddi  26300  abliso  26303  ogrpaddltrbid  26328  ogrpinvlt  26331  archiabllem1a  26352  archiabllem1  26354  archiabllem2c  26356  slmdvs0  26385  dvrcan5  26405  ornglmullt  26419  orngrmullt  26420  rhmunitinv  26434  qqhval2lem  26554  esummulc1  26674  measxun2  26768  measssd  26773  oddpwdc  26880  eulerpartlemgs2  26906  eulerpartlemn  26907  totprobd  26952  signstfvn  27113  signstfveq0  27121  zetacvg  27144  lgamgulmlem4  27161  lgamcvg2  27184  gamp1  27187  subfaclim  27219  cvxscon  27275  rescon  27278  cvmliftmolem1  27313  cvmliftlem7  27323  cvmliftlem13  27328  cvmlift2lem7  27341  cvmlift3lem5  27355  ghomf1olem  27456  fprodm1  27620  fallfacfwd  27682  binomfallfaclem2  27686  faclim2  27697  funsseq  27723  bpolydiflem  28340  bpoly4  28345  fsumcube  28346  ptrest  28572  itg2addnclem  28590  itg2addnclem3  28592  itgaddnclem2  28598  itgsubnc  28601  iblmulc2nc  28604  itgabsnc  28608  ftc2nc  28623  areacirclem1  28631  areacirclem4  28634  areacirc  28636  clsun  28670  topjoin  28733  cocanfo  28758  ablo4pnp  28892  zerdivemp1x  28908  crngm4  28950  crngohomfo  28953  diophrw  29244  eldioph2lem1  29245  pellexlem2  29318  pellexlem6  29322  pellex  29323  pell1234qrne0  29341  pell1234qrreccl  29342  pell1qrgaplem  29361  rmxm1  29422  oddcomabszz  29432  jm2.19lem1  29485  jm3.1lem2  29514  dnnumch3  29547  pwssplit4  29589  flcidc  29678  hashgcdlem  29712  deg1mhm  29722  itgpowd  29737  dvsconst  29751  dvsid  29752  expgrowth  29756  itgsinexplem1  29941  itgsinexp  29942  stoweidlem1  29943  wallispi2lem2  30014  stirlinglem3  30018  stirlinglem5  30020  stirlinglem10  30025  stirlinglem15  30030  sigaradd  30049  cevathlem1  30050  imarnf1pr  30297  powm2modprm  30395  usgrauvtxvd  30677  frgrancvvdeq  30782  frgrancvvdgeq  30783  numclwwlk7  30854  cpmadugsumlemF  31347  bnj1379  32141  bnj1321  32335  bj-bary1lem  32922  fsumshftdOLD  32926  lfl0  33033  lfladd  33034  lflmul  33036  eqlkr3  33069  olm11  33195  latm12  33198  cmtcomlemN  33216  omlspjN  33229  hlatj12  33338  1cvrjat  33442  dalemrotyz  33625  padd12N  33806  pmapjlln1  33822  atmod2i1  33828  pmapocjN  33897  pnonsingN  33900  pexmidN  33936  lhp2at0  33999  lhpelim  34004  ltrncnv  34113  ltrnmw  34118  cdleme7c  34212  cdleme15b  34242  cdlemednpq  34266  cdleme20y  34269  cdleme20m  34290  cdleme22cN  34309  cdleme22d  34310  cdleme23b  34317  cdleme30a  34345  cdleme35h  34423  cdlemeg46frv  34492  cdlemg2fv2  34567  cdlemg2l  34570  cdlemg2m  34571  cdlemg8c  34596  cdlemg10bALTN  34603  cdlemg12  34617  cdlemg13a  34618  cdlemg18c  34647  cdlemg19  34651  trlcoat  34690  cdlemg47  34703  tendo1ne0  34795  cdlemk9  34806  cdlemk9bN  34807  dia2dimlem1  35032  tendolinv  35073  tendorinv  35074  dvhlveclem  35076  doca3N  35095  dihmeetlem7N  35278  dihjatc1  35279  dihmeetlem18N  35292  dochnoncon  35359  dihjatc  35385  dihjatcclem1  35386  dihjatcclem4  35389  dochsnkr  35440  lcfl7lem  35467  lcfl8  35470  lcfl9a  35473  lclkrlem1  35474  lclkrlem2e  35479  lclkrlem2j  35484  lcfrlem1  35510  lcfrlem9  35518  lcfrlem23  35533  lcfrlem31  35541  mapd0  35633  mapdpglem21  35660  baerlem3lem1  35675  baerlem5alem1  35676  mapdindp4  35691  mapdh6gN  35710  hdmap1l6g  35785  hgmapval0  35863  hgmaprnlem1N  35867  hlhilhillem  35931
  Copyright terms: Public domain W3C validator