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

Theorem 3eqtr3d 2473
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 2467 . 2  |-  ( ph  ->  B  =  C )
4 3eqtr3d.3 . 2  |-  ( ph  ->  B  =  D )
53, 4eqtr3d 2467 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1362
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-ex 1590  df-cleq 2426
This theorem is referenced by:  mpteqb  5776  fvmptt  5777  fsnunfv  5905  f1ocnvfv1  5970  f1ocnvfv2  5971  fcof1  5978  weniso  6032  caov12d  6273  caov13d  6275  caov411d  6277  caovmo  6289  grprinvlem  6290  grprinvd  6291  grpridd  6292  onovuni  6789  tfrlem5  6825  seqomlem1  6891  seqomlem4  6894  onasuc  6956  onesuc  6958  oeeui  7029  fopwdom  7407  unxpdomlem2  7506  cantnfres  7873  cnfcom2lem  7922  cnfcom2  7923  cnfcom2lemOLD  7930  cnfcom2OLD  7931  cardiun  8140  ackbij1lem16  8392  ackbij2lem2  8397  fpwwe2lem6  8789  fpwwe2lem8  8791  canthp1lem2  8807  mul12  9522  mul4  9525  addid1  9536  addcan  9540  addcom  9542  addcomd  9558  add12  9569  ppncan  9638  addsub4  9639  muladd  9764  mulcand  9956  receu  9968  div13  10002  divdivdiv  10019  divcan5  10020  divdiv1  10029  divdiv2  10030  halfaddsub  10545  uzindOLD  10723  xadddi  11245  xov1plusxeqvd  11417  fztp  11496  flzadd  11654  fldiv  11682  addmodid  11731  modnegd  11737  modsub12d  11739  2submod  11743  seqm1  11806  seqcaopr  11826  seqf1o  11830  expsub  11894  zesq  11970  digit1  11981  discr1  11983  discr  11984  facnn2  12043  faclbnd6  12058  hashfz1  12100  hashdom  12125  hashun  12128  hashbclem  12188  hashfac  12194  seqcoll  12199  wrdlenccats1lenm1  12288  ccatopth  12347  repsw2  12533  repsw3  12534  shftval3  12548  crre  12586  resub  12599  imsub  12607  cjsub  12621  abslem2  12810  sqreulem  12830  climshft2  13043  isercolllem2  13126  iseraltlem2  13143  iseraltlem3  13144  fsumsub  13237  fsumtscopo  13247  fsumtscopo2  13248  hashiun  13267  bcxmas  13280  climcndslem1  13294  climcndslem2  13295  trireciplem  13306  geoser  13311  geo2sum2  13316  sinsub  13434  cossub  13435  rpnnen2lem10  13488  ruclem12  13505  divalglem9  13587  bitsinv1lem  13619  bitsinv1  13620  bitsf1  13624  sadasslem  13648  bitsres  13651  smup1  13667  smumul  13671  modgcd  13702  absmulgcd  13713  gcdmultiplez  13717  eucalg  13744  numdensq  13814  dfphi2  13831  phiprm  13834  fermltl  13841  prmdiveq  13843  odzdvds  13849  modprm0  13855  coprimeprodsq  13858  pythagtriplem6  13870  pythagtriplem7  13871  pythagtriplem12  13875  pythagtriplem16  13879  pcaddlem  13932  sumhash  13940  pcfac  13943  pockthlem  13948  prmreclem6  13964  4sqlem12  13999  4sqlem15  14002  vdwlem3  14026  vdwlem6  14029  vdwlem9  14032  ramub1lem2  14070  cshwshashlem2  14105  divsaddvallem  14471  xpsaddlem  14495  xpsvsca  14499  mrcun  14542  homfeqval  14618  comfeqval  14629  sectcan  14676  sectco  14677  sectmon  14698  monsect  14699  funcsect  14764  setcmon  14937  resscatc  14955  catciso  14957  evlfcllem  15013  curf2cl  15023  curfcl  15024  yonedalem4c  15069  yonedalem3b  15071  yonedainv  15073  latj12  15248  mnd12g  15407  resmhm  15468  pwsco2mhm  15480  frmdup3  15523  grprcan  15550  grplcan  15569  grpinv11  15574  grpinvnz  15576  grplmulf1o  15579  grpinvpropd  15580  grpinvadd  15583  grpsubsub4  15597  mulgz  15627  mulgdirlem  15630  mulgdir  15631  mulgass  15636  mulgsubdir  15637  mulgpropd  15639  pwsmulg  15648  imasgrp2  15649  isnsg3  15694  nmzsubg  15701  ssnmz  15702  eqger  15710  eqglact  15711  ghminv  15733  conjnmz  15759  subgga  15797  gasubg  15799  galcan  15801  gacan  15802  cntzsubg  15833  cntzmhm  15835  psgnunilem2  15980  sylow1lem1  16076  sylow2blem2  16099  sylow2blem3  16100  lsmmod  16151  lsmpropd  16153  lsmdisj2  16158  subgdisj1  16167  subgdisj2  16168  efgredleme  16219  efgredlemd  16220  efgredlemc  16221  efgredlem  16223  frgpup3lem  16253  mulgdi  16293  lsm4  16321  cygabl  16346  gsummhm2  16410  gsummhm2OLD  16411  gsumpt  16428  gsumptOLD  16429  gsum2d  16436  gsum2dOLD  16437  dprdfeq0  16485  dprdfeq0OLD  16492  ablfac1eu  16547  rngcom  16608  isrngd  16614  rnglz  16616  rngrz  16617  rng1eq0  16618  rngmneg1  16621  gsumdixpOLD  16634  gsumdixp  16635  unitgrp  16692  irredrmul  16732  drngmul0or  16776  subrginv  16804  subrgunit  16806  srngnvl  16864  srngadd  16865  srngmul  16866  issrngd  16869  lmodvs0  16905  lmodvneg1  16911  lmodcom  16914  lmodsubdi  16925  lmodvsinv  17038  lmodvsinv2  17039  lmhmvsca  17047  lvecvs0or  17110  lvecinv  17115  lspsnvs  17116  lspabs2  17122  lspfixed  17130  lspsolv  17145  unitrrg  17286  asclpropd  17337  psrass1lem  17380  psrlidm  17407  psrlidmOLD  17408  psrridm  17409  psrridmOLD  17410  mvrf1  17431  mplmon2mul  17514  coe1pwmul  17629  prmirredlem  17758  prmirredlemOLD  17761  mulgrhm2  17768  mulgrhm2OLD  17771  chrrhm  17803  znidomb  17835  psgnghm  17851  psgninv  17853  zrhpsgnodpm  17863  evpmodpmf1o  17867  psgndiflemB  17871  ip0r  17907  ipdir  17909  ipdi  17910  ipass  17915  ipassr  17916  phlpropd  17925  ocvpj  17983  uvcresum  18059  lmimlbs  18106  gsumcom3  18140  mat0dimbas0  18166  mdetrlin  18250  mdetrsca  18251  mdetr0  18253  mdetunilem8  18266  mdetuni0  18268  mdetmul  18270  maducoeval2  18287  madurid  18291  madulid  18292  matinv  18324  matunit  18325  slesolinv  18327  slesolinvbi  18328  restin  18611  cncmp  18836  cmpsublem  18843  conndisj  18861  cnconn  18867  kgencmp2  18960  ufldom  19376  tgplacthmeo  19515  ghmcnp  19526  divstgpopn  19531  divstgphaus  19534  tsmsxplem2  19569  tususp  19688  xpsdsval  19797  blpnfctr  19852  xmssym  19881  ressxms  19941  isngp2  20030  ngppropd  20064  nminvr  20091  blcvx  20216  icccvx  20363  pcohtpylem  20432  pcohtpy  20433  cvsmuleqdivd  20524  cvsdiveqd  20525  pjthlem1  20765  ovollb2lem  20812  ovolicc2lem1  20841  ovolicc2lem5  20845  volsup  20878  ovolioo  20890  uniiccdif  20899  uniioombllem3  20906  uniioombllem4  20907  vitalilem3  20931  itg1sub  21028  itg2const  21059  iblcnlem1  21106  itgcnlem  21108  itgaddlem2  21142  itgsub  21144  itgabs  21153  ditgsplit  21177  dvmulbr  21254  dvcmul  21259  dvcmulf  21260  dvrec  21270  dvmptres3  21271  dvmptadd  21275  dvmptmul  21276  dvmptres2  21277  dvmptneg  21281  dvmptsub  21282  dvmptcj  21283  dvmptco  21287  dveflem  21292  dvlip  21306  dvlipcn  21307  dvlip2  21308  dvcvx  21333  dvfsumle  21334  dvfsumabs  21336  dvfsumlem1  21339  dvfsumlem2  21340  ftc2  21357  ftc2ditglem  21358  itgparts  21360  itgsubstlem  21361  itgsubst  21362  evlslem1  21366  evlseu  21367  evlssca  21373  evlsvar  21374  pf1ind  21405  fta1glem1  21521  fta1blem  21524  plyeq0lem  21562  plymullem1  21566  coeeulem  21576  coe0  21607  coesub  21608  dvply1  21634  plydivlem4  21646  plyrem  21655  fta1lem  21657  vieta1  21662  plyexmo  21663  elqaalem2  21670  aareccl  21676  aannenlem1  21678  aaliou3lem2  21693  dvtaylp  21719  taylthlem1  21722  radcnvlem1  21762  pserdvlem2  21777  efcvx  21798  ptolemy  21842  tangtx  21851  efif1olem3  21884  efif1olem4  21885  lognegb  21922  efiarg  21940  cosargd  21941  tanarg  21952  logtayl  21989  cxpsub  22011  cxproot  22019  cxpsqr  22032  cxpcn3lem  22069  cxpaddlelem  22073  abscxpbnd  22075  root1eq1  22077  cxpeq  22079  logrec  22099  isosctrlem2  22101  isosctrlem3  22102  isosctr  22103  ssscongptld  22104  chordthmlem  22111  heron  22117  quad2  22118  dcubic1lem  22122  mcubic  22126  cubic2  22127  cubic  22128  dquartlem2  22131  dquart  22132  quart1lem  22134  quart1  22135  asinlem2  22148  asinlem3  22150  asinsin  22171  sinacos  22184  atanlogsublem  22194  efiatan2  22196  2efiatan  22197  tanatan  22198  atantan  22202  atans2  22210  dvatan  22214  atantayl  22216  atantayl2  22217  log2cnv  22223  rlimcnp2  22244  cxplim  22249  cxp2lim  22254  cvxcl  22262  scvxcvx  22263  wilthlem1  22290  wilthlem2  22291  ftalem5  22298  basellem3  22304  basellem5  22306  basellem8  22309  mumullem2  22402  musum  22415  musumsum  22416  muinv  22417  sgmppw  22420  1sgmprm  22422  1sgm2ppw  22423  ppiub  22427  logfac2  22440  chpchtsum  22442  perfectlem1  22452  perfectlem2  22453  dchrn0  22473  dchrfi  22478  dchrabs  22483  dchrptlem1  22487  dchrhash  22494  dchr2sum  22496  sum2dchr  22497  bposlem6  22512  bposlem9  22515  lgsvalmod  22538  lgsdilem  22545  lgsne0  22556  lgssq  22558  lgssq2  22559  lgsqr  22569  lgsdchrval  22570  lgsdchr  22571  lgseisenlem1  22572  lgseisenlem2  22573  lgseisenlem4  22575  lgsquadlem1  22577  lgsquadlem3  22579  lgsquad3  22584  m1lgs  22585  rplogsumlem1  22617  rplogsumlem2  22618  dchrisumlem2  22623  dchrisum0fno1  22644  rpvmasum2  22645  dchrisum0lem1  22649  dchrisum0lem2  22651  mudivsum  22663  mulog2sumlem1  22667  vmalogdivsum  22672  2vmadivsumlem  22673  logsqvma  22675  selberglem2  22679  selberg2lem  22683  selberg3lem1  22690  selberg4lem1  22693  selberg4  22694  pntrsumo1  22698  selbergr  22701  selberg34r  22704  pntrlog2bndlem3  22712  pntrlog2bndlem4  22713  pntibndlem2  22724  pntlemg  22731  pntlemr  22735  pntlemf  22738  ostthlem1  22760  padicabvcxp  22765  ostth3  22771  tgcgrcomlr  22818  tgbtwnconn1lem2  22880  tgbtwnconn1lem3  22881  f1otrg  22939  ttgcontlem1  22953  brbtwn2  22973  axsegconlem10  22994  ax5seglem3  22999  ax5seglem6  23002  axpaschlem  23008  axeuclidlem  23030  axcontlem2  23033  axcontlem7  23038  axcontlem8  23039  cusgrasizeindslem3  23205  grpoidinvlem1  23513  grpoideu  23518  grporcan  23530  grpolcan  23542  grpoasscan1  23546  grpoinvop  23550  grpopnpcan2  23562  gxsuc  23581  gxsub  23585  gxmul  23587  ablo4  23596  subgoinv  23617  ablomul  23664  ghgrp  23677  ghablo  23678  rngolz  23710  rngorz  23711  zerdivemp1  23743  nvadd12  23823  nvscom  23831  nvmul0or  23854  nvz0  23878  smcnlem  23914  ipidsq  23930  sspz  23955  lno0  23978  lnoadd  23980  lnomul  23982  ipasslem3  24055  dipdi  24065  dipassr  24068  dipsubdi  24071  ubthlem2  24094  hvmul0or  24249  hvadd12  24259  hvadd4  24260  hvmulcom  24267  normneg  24368  pjhthlem1  24616  chj12  24759  spanunsni  24804  5oalem2  24880  3oalem2  24888  mayete3iOLD  24954  hoadd4  25010  homul12  25031  hosubdi  25034  honegsubdi  25036  hosub4  25039  adj2  25160  lnopmul  25193  lnopaddi  25197  lnfnaddi  25269  lnfnmuli  25270  cnlnadjlem6  25298  adjeq0  25317  leopmul  25360  opsqrlem1  25366  opsqrlem6  25371  hstnmoc  25449  strlem1  25476  chirredlem3  25618  fpwrelmapffslem  25856  xaddeq0  25870  bcm1n  25901  divnumden2  25909  xmulcand  25918  xreceu  25919  xrsmulgzz  25961  xrge0adddir  25978  xrge0adddi  25979  abliso  25982  ogrpaddltrbid  26007  ogrpinvlt  26010  archiabllem1a  26031  archiabllem1  26033  archiabllem2c  26035  slmdvs0  26089  dvrcan5  26113  ornglmullt  26127  orngrmullt  26128  rhmunitinv  26142  qqhval2lem  26263  esummulc1  26383  measxun2  26477  measssd  26482  oddpwdc  26584  eulerpartlemgs2  26610  eulerpartlemn  26611  totprobd  26656  signstfvn  26817  signstfveq0  26825  zetacvg  26848  lgamgulmlem4  26865  lgamcvg2  26888  gamp1  26891  subfaclim  26923  cvxscon  26979  rescon  26982  cvmliftmolem1  27017  cvmliftlem7  27027  cvmliftlem13  27032  cvmlift2lem7  27045  cvmlift3lem5  27059  ghomf1olem  27159  fprodm1  27323  fallfacfwd  27385  binomfallfaclem2  27389  faclim2  27400  funsseq  27426  bpolydiflem  28043  bpoly4  28048  fsumcube  28049  ptrest  28266  itg2addnclem  28284  itg2addnclem3  28286  itgaddnclem2  28292  itgsubnc  28295  iblmulc2nc  28298  itgabsnc  28302  ftc2nc  28317  areacirclem1  28325  areacirclem4  28328  areacirc  28330  clsun  28364  topjoin  28427  cocanfo  28452  ablo4pnp  28586  zerdivemp1x  28602  crngm4  28644  crngohomfo  28647  diophrw  28939  eldioph2lem1  28940  pellexlem2  29013  pellexlem6  29017  pellex  29018  pell1234qrne0  29036  pell1234qrreccl  29037  pell1qrgaplem  29056  rmxm1  29117  oddcomabszz  29127  jm2.19lem1  29180  jm3.1lem2  29209  dnnumch3  29242  pwssplit4  29284  flcidc  29373  hashgcdlem  29407  deg1mhm  29417  itgpowd  29432  dvsconst  29446  dvsid  29447  expgrowth  29451  itgsinexplem1  29637  itgsinexp  29638  stoweidlem1  29639  wallispi2lem2  29710  stirlinglem3  29714  stirlinglem5  29716  stirlinglem10  29721  stirlinglem15  29726  sigaradd  29745  cevathlem1  29746  imarnf1pr  29993  powm2modprm  30091  usgrauvtxvd  30373  frgrancvvdeq  30478  frgrancvvdgeq  30479  numclwwlk7  30550  bnj1379  31523  bnj1321  31717  bj-bary1lem  32171  lfl0  32280  lfladd  32281  lflmul  32283  eqlkr3  32316  olm11  32442  latm12  32445  cmtcomlemN  32463  omlspjN  32476  hlatj12  32585  1cvrjat  32689  dalemrotyz  32872  padd12N  33053  pmapjlln1  33069  atmod2i1  33075  pmapocjN  33144  pnonsingN  33147  pexmidN  33183  lhp2at0  33246  lhpelim  33251  ltrncnv  33360  ltrnmw  33365  cdleme7c  33459  cdleme15b  33489  cdlemednpq  33513  cdleme20y  33516  cdleme20m  33537  cdleme22cN  33556  cdleme22d  33557  cdleme23b  33564  cdleme30a  33592  cdleme35h  33670  cdlemeg46frv  33739  cdlemg2fv2  33814  cdlemg2l  33817  cdlemg2m  33818  cdlemg8c  33843  cdlemg10bALTN  33850  cdlemg12  33864  cdlemg13a  33865  cdlemg18c  33894  cdlemg19  33898  trlcoat  33937  cdlemg47  33950  tendo1ne0  34042  cdlemk9  34053  cdlemk9bN  34054  dia2dimlem1  34279  tendolinv  34320  tendorinv  34321  dvhlveclem  34323  doca3N  34342  dihmeetlem7N  34525  dihjatc1  34526  dihmeetlem18N  34539  dochnoncon  34606  dihjatc  34632  dihjatcclem1  34633  dihjatcclem4  34636  dochsnkr  34687  lcfl7lem  34714  lcfl8  34717  lcfl9a  34720  lclkrlem1  34721  lclkrlem2e  34726  lclkrlem2j  34731  lcfrlem1  34757  lcfrlem9  34765  lcfrlem23  34780  lcfrlem31  34788  mapd0  34880  mapdpglem21  34907  baerlem3lem1  34922  baerlem5alem1  34923  mapdindp4  34938  mapdh6gN  34957  hdmap1l6g  35032  hgmapval0  35110  hgmaprnlem1N  35114  hlhilhillem  35178
  Copyright terms: Public domain W3C validator