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

Theorem 3eqtr3d 2336
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 2330 . 2  |-  ( ph  ->  B  =  C )
4 3eqtr3d.3 . 2  |-  ( ph  ->  B  =  D )
53, 4eqtr3d 2330 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632
This theorem is referenced by:  mpteqb  5630  fvmptt  5631  fsnunfv  5736  f1ocnvfv1  5808  f1ocnvfv2  5809  fcof1  5813  weniso  5868  caov12d  6057  caov13d  6059  caov411d  6061  caovmo  6073  grprinvlem  6074  grprinvd  6075  grpridd  6076  onovuni  6375  seqomlem1  6478  seqomlem4  6481  onasuc  6543  onesuc  6545  oeeui  6616  fopwdom  6986  unxpdomlem2  7084  cantnfres  7395  cnfcom2lem  7420  cnfcom2  7421  cardiun  7631  ackbij1lem16  7877  ackbij2lem2  7882  fpwwe2lem6  8273  fpwwe2lem8  8275  canthp1lem2  8291  mul12  8994  mul4  8997  addid1  9008  addcan  9012  addcom  9014  addcomd  9030  add12  9041  ppncan  9105  addsub4  9106  muladd  9228  mulcand  9417  receu  9429  div13  9461  divdivdiv  9477  divcan5  9478  divdiv1  9487  divdiv2  9488  halfaddsub  9961  uzindOLD  10122  xadddi  10631  xov1plusxeqvd  10796  fztp  10857  flzadd  10967  fldiv  10980  modnegd  11020  modsub12d  11022  seqm1  11079  seqcaopr  11099  seqf1o  11103  expsub  11165  zesq  11240  digit1  11251  discr1  11253  discr  11254  facnn2  11313  faclbnd6  11328  hashfz1  11361  hashdom  11377  hashun  11380  hashbclem  11406  hashfac  11412  seqcoll  11417  ccatopth  11478  shftval3  11587  crre  11615  resub  11628  imsub  11636  cjsub  11650  abslem2  11839  sqreulem  11859  climshft2  12072  isercolllem2  12155  iseraltlem2  12171  iseraltlem3  12172  fsumsub  12266  fsumtscopo  12276  fsumtscopo2  12277  hashiun  12296  bcxmas  12310  climcndslem1  12324  climcndslem2  12325  trireciplem  12336  geoser  12341  geo2sum2  12346  sinsub  12464  cossub  12465  rpnnen2lem10  12518  ruclem12  12535  divalglem9  12616  bitsinv1lem  12648  bitsinv1  12649  bitsf1  12653  sadasslem  12677  bitsres  12680  smup1  12696  smumul  12700  modgcd  12731  absmulgcd  12742  gcdmultiplez  12746  eucalg  12773  numdensq  12841  dfphi2  12858  phiprm  12861  fermltl  12868  prmdiveq  12870  odzdvds  12876  coprimeprodsq  12878  pythagtriplem6  12890  pythagtriplem7  12891  pythagtriplem12  12895  pythagtriplem16  12899  pcaddlem  12952  sumhash  12960  pcfac  12963  pockthlem  12968  prmreclem6  12984  4sqlem12  13019  4sqlem15  13022  vdwlem3  13046  vdwlem6  13049  vdwlem9  13052  ramub1lem2  13090  divsaddvallem  13469  xpsaddlem  13493  xpsvsca  13497  mrcun  13540  homfeqval  13616  comfeqval  13627  sectcan  13674  sectco  13675  sectmon  13696  monsect  13697  funcsect  13762  setcmon  13935  resscatc  13953  catciso  13955  evlfcllem  14011  curf2cl  14021  curfcl  14022  yonedalem4c  14067  yonedalem3b  14069  yonedainv  14071  latj12  14218  mnd12g  14393  resmhm  14452  pwsco2mhm  14463  frmdup3  14504  grprcan  14531  grplcan  14550  grpinv11  14553  grpinvnz  14555  grplmulf1o  14558  grpinvpropd  14559  grpinvadd  14560  grpsubsub4  14574  mulgz  14604  mulgdirlem  14607  mulgdir  14608  mulgass  14613  mulgsubdir  14614  mulgpropd  14616  pwsmulg  14625  imasgrp2  14626  isnsg3  14667  nmzsubg  14674  ssnmz  14675  eqger  14683  eqglact  14684  ghminv  14706  conjnmz  14732  subgga  14770  gasubg  14772  galcan  14774  gacan  14775  cntzsubg  14828  cntzmhm  14830  sylow1lem1  14925  sylow2blem2  14948  sylow2blem3  14949  lsmmod  15000  lsmpropd  15002  lsmdisj2  15007  subgdisj1  15016  subgdisj2  15017  efgredleme  15068  efgredlemd  15069  efgredlemc  15070  efgredlem  15072  frgpup3lem  15102  mulgdi  15142  lsm4  15168  cygabl  15193  gsummhm2  15228  gsumpt  15238  gsum2d  15239  dprdfeq0  15273  ablfac1eu  15324  rngcom  15385  isrngd  15391  rnglz  15393  rngrz  15394  rng1eq0  15395  rngmneg1  15398  gsumdixp  15408  unitgrp  15465  irredrmul  15505  drngmul0or  15549  subrginv  15577  subrgunit  15579  srngnvl  15637  srngadd  15638  srngmul  15639  issrngd  15642  lmodvs0  15680  lmodvneg1  15683  lmodvsnegOLD  15684  lmodcom  15687  lmodsubdi  15698  lmodvsinv  15809  lmodvsinv2  15810  lmhmvsca  15818  lvecvs0or  15877  lvecinv  15882  lspsnvs  15883  lspabs2  15889  lspfixed  15897  lspsolv  15912  unitrrg  16050  asclpropd  16101  psrass1lem  16139  psrlidm  16164  psrridm  16165  mvrf1  16186  mplmon2mul  16258  coe1pwmul  16371  prmirredlem  16462  mulgrhm2  16477  chrrhm  16501  znidomb  16531  ip0r  16557  ipdir  16559  ipdi  16560  ipass  16565  ipassr  16566  phlpropd  16575  ocvpj  16633  restin  16913  cncmp  17135  cmpsublem  17142  conndisj  17158  cnconn  17164  kgencmp2  17257  ufldom  17673  tgplacthmeo  17802  ghmcnp  17813  divstgpopn  17818  divstgphaus  17821  tsmsxplem2  17852  xpsdsval  17961  blpnfctr  17998  xmssym  18027  ressxms  18087  isngp2  18135  ngppropd  18169  nminvr  18196  blcvx  18320  icccvx  18464  pcohtpylem  18533  pcohtpy  18534  pjthlem1  18817  ovollb2lem  18863  ovolicc2lem1  18892  ovolicc2lem5  18896  volsup  18929  ovolioo  18941  uniiccdif  18949  uniioombllem3  18956  uniioombllem4  18957  vitalilem3  18981  itg1sub  19080  itg2const  19111  iblcnlem1  19158  itgcnlem  19160  itgaddlem2  19194  itgsub  19196  itgabs  19205  ditgsplit  19227  dvmulbr  19304  dvcmul  19309  dvcmulf  19310  dvrec  19320  dvmptres3  19321  dvmptadd  19325  dvmptmul  19326  dvmptres2  19327  dvmptneg  19331  dvmptsub  19332  dvmptcj  19333  dvmptco  19337  dveflem  19342  dvlip  19356  dvlipcn  19357  dvlip2  19358  dvcvx  19383  dvfsumle  19384  dvfsumabs  19386  dvfsumlem1  19389  dvfsumlem2  19390  ftc2  19407  ftc2ditglem  19408  itgparts  19410  itgsubstlem  19411  itgsubst  19412  evlslem1  19415  evlseu  19416  evlssca  19422  evlsvar  19423  pf1ind  19454  fta1glem1  19567  fta1blem  19570  plyeq0lem  19608  plymullem1  19612  coeeulem  19622  coe0  19653  coesub  19654  dvply1  19680  plydivlem4  19692  plyrem  19701  fta1lem  19703  vieta1  19708  plyexmo  19709  elqaalem2  19716  aareccl  19722  aannenlem1  19724  aaliou3lem2  19739  dvtaylp  19765  taylthlem1  19768  radcnvlem1  19805  pserdvlem2  19820  efcvx  19841  tangtx  19889  efif1olem3  19922  efif1olem4  19923  lognegb  19959  efiarg  19977  cosargd  19978  tanarg  19986  logtayl  20023  cxpsub  20045  cxproot  20053  cxpsqr  20066  cxpcn3lem  20103  cxpaddlelem  20107  abscxpbnd  20109  root1eq1  20111  cxpeq  20113  logrec  20133  isosctrlem2  20135  isosctrlem3  20136  isosctr  20137  ssscongptld  20138  chordthmlem  20145  quad2  20151  dcubic1lem  20155  mcubic  20159  cubic2  20160  cubic  20161  dquartlem2  20164  dquart  20165  quart1lem  20167  quart1  20168  asinlem2  20181  asinlem3  20183  asinsin  20204  sinacos  20217  atanlogsublem  20227  efiatan2  20229  2efiatan  20230  tanatan  20231  atantan  20235  atans2  20243  dvatan  20247  atantayl  20249  atantayl2  20250  log2cnv  20256  rlimcnp2  20277  cxplim  20282  cxp2lim  20287  cvxcl  20295  scvxcvx  20296  wilthlem1  20322  wilthlem2  20323  ftalem5  20330  basellem3  20336  basellem5  20338  basellem8  20341  mumullem2  20434  musum  20447  musumsum  20448  muinv  20449  sgmppw  20452  1sgmprm  20454  1sgm2ppw  20455  ppiub  20459  logfac2  20472  chpchtsum  20474  perfectlem1  20484  perfectlem2  20485  dchrn0  20505  dchrfi  20510  dchrabs  20515  dchrptlem1  20519  dchrhash  20526  dchr2sum  20528  sum2dchr  20529  bposlem6  20544  bposlem9  20547  lgsvalmod  20570  lgsdilem  20577  lgsne0  20588  lgssq  20590  lgssq2  20591  lgsqr  20601  lgsdchrval  20602  lgsdchr  20603  lgseisenlem1  20604  lgseisenlem2  20605  lgseisenlem4  20607  lgsquadlem1  20609  lgsquadlem3  20611  lgsquad3  20616  m1lgs  20617  rplogsumlem1  20649  rplogsumlem2  20650  dchrisumlem2  20655  dchrisum0fno1  20676  rpvmasum2  20677  dchrisum0lem1  20681  dchrisum0lem2  20683  mudivsum  20695  mulog2sumlem1  20699  vmalogdivsum  20704  2vmadivsumlem  20705  logsqvma  20707  selberglem2  20711  selberg2lem  20715  selberg3lem1  20722  selberg4lem1  20725  selberg4  20726  pntrsumo1  20730  selbergr  20733  selberg34r  20736  pntrlog2bndlem3  20744  pntrlog2bndlem4  20745  pntibndlem2  20756  pntlemg  20763  pntlemr  20767  pntlemf  20770  ostthlem1  20792  padicabvcxp  20797  ostth3  20803  grpoidinvlem1  20887  grpoideu  20892  grporcan  20904  grpolcan  20916  grpoasscan1  20920  grpoinvop  20924  grpopnpcan2  20936  gxsuc  20955  gxsub  20959  gxmul  20961  ablo4  20970  subgoinv  20991  ablomul  21038  ghgrp  21051  ghablo  21052  rngolz  21084  rngorz  21085  nvadd12  21195  nvscom  21203  nvmul0or  21226  nvz0  21250  smcnlem  21286  ipidsq  21302  sspz  21327  lno0  21350  lnoadd  21352  lnomul  21354  ipasslem3  21427  dipdi  21437  dipassr  21440  dipsubdi  21443  ubthlem2  21466  hvmul0or  21620  hvadd12  21630  hvadd4  21631  hvmulcom  21638  normneg  21739  pjhthlem1  21986  chj12  22129  spanunsni  22174  5oalem2  22250  3oalem2  22258  mayete3iOLD  22324  hoadd4  22380  homul12  22401  hosubdi  22404  honegsubdi  22406  hosub4  22409  adj2  22530  lnopmul  22563  lnopaddi  22567  lnfnaddi  22639  lnfnmuli  22640  cnlnadjlem6  22668  adjeq0  22687  leopmul  22730  opsqrlem1  22736  opsqrlem6  22741  hstnmoc  22819  strlem1  22846  chirredlem3  22988  bcm1n  23048  xmulcand  23120  xreceu  23121  xaddeq0  23319  xrsmulgzz  23322  xrge0adddir  23347  esummulc1  23464  measxun2  23553  measssd  23558  totprobd  23644  zetacvg  23704  subfaclim  23734  cvxscon  23789  rescon  23792  cvmliftmolem1  23827  cvmliftlem7  23837  cvmliftlem13  23842  cvmlift2lem7  23855  cvmlift3lem5  23869  ghomf1olem  24016  faclimlem9  24125  funsseq  24196  brbtwn2  24605  axsegconlem10  24626  ax5seglem3  24631  ax5seglem6  24634  axpaschlem  24640  axeuclidlem  24662  axcontlem2  24665  axcontlem7  24670  axcontlem8  24671  bpolydiflem  24861  bpoly4  24866  fsumcube  24867  itg2addnclem  25003  itg2addnc  25005  itgaddnclem2  25010  itgsubnc  25013  iblmulc2nc  25016  itgabsnc  25020  areacirclem2  25028  areacirclem5  25032  areacirc  25034  multinvb  25526  zerdivemp1  25539  mslb1  25710  trnij  25718  addcanrg  25770  idsubfun  25961  clsun  26349  topjoin  26417  cocanfo  26477  ablo4pnp  26673  zerdivemp1x  26689  crngm4  26731  crngohomfo  26734  diophrw  26941  eldioph2lem1  26942  pellexlem2  27018  pellexlem6  27022  pellex  27023  pell1234qrne0  27041  pell1234qrreccl  27042  pell1qrgaplem  27061  rmxm1  27122  oddcomabszz  27132  jm2.19lem1  27185  jm3.1lem2  27214  dnnumch3  27247  pwssplit4  27294  uvcresum  27345  lmimlbs  27409  flcidc  27482  psgnunilem2  27521  psgnghm  27540  gsumcom3  27557  hashgcdlem  27619  deg1mhm  27629  dvsconst  27650  dvsid  27651  expgrowth  27655  itgsinexplem1  27851  sigaradd  27959  cevathlem1  27960  bnj1379  29179  bnj1321  29373  lfl0  29877  lfladd  29878  lflmul  29880  eqlkr3  29913  olm11  30039  latm12  30042  cmtcomlemN  30060  omlspjN  30073  hlatj12  30182  1cvrjat  30286  dalemrotyz  30469  padd12N  30650  pmapjlln1  30666  atmod2i1  30672  pmapocjN  30741  pnonsingN  30744  pexmidN  30780  lhp2at0  30843  lhpelim  30848  ltrncnv  30957  ltrnmw  30962  cdleme7c  31056  cdleme15b  31086  cdlemednpq  31110  cdleme20y  31113  cdleme20m  31134  cdleme22cN  31153  cdleme22d  31154  cdleme23b  31161  cdleme30a  31189  cdleme35h  31267  cdlemeg46frv  31336  cdlemg2fv2  31411  cdlemg2l  31414  cdlemg2m  31415  cdlemg8c  31440  cdlemg10bALTN  31447  cdlemg12  31461  cdlemg13a  31462  cdlemg18c  31491  cdlemg19  31495  trlcoat  31534  cdlemg47  31547  tendo1ne0  31639  cdlemk9  31650  cdlemk9bN  31651  dia2dimlem1  31876  tendolinv  31917  tendorinv  31918  dvhlveclem  31920  doca3N  31939  dihmeetlem7N  32122  dihjatc1  32123  dihmeetlem18N  32136  dochnoncon  32203  dihjatc  32229  dihjatcclem1  32230  dihjatcclem4  32233  dochsnkr  32284  lcfl7lem  32311  lcfl8  32314  lcfl9a  32317  lclkrlem1  32318  lclkrlem2e  32323  lclkrlem2j  32328  lcfrlem1  32354  lcfrlem9  32362  lcfrlem23  32377  lcfrlem31  32385  mapd0  32477  mapdpglem21  32504  baerlem3lem1  32519  baerlem5alem1  32520  mapdindp4  32535  mapdh6gN  32554  hdmap1l6g  32629  hgmapval0  32707  hgmaprnlem1N  32711  hlhilhillem  32775
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-cleq 2289
  Copyright terms: Public domain W3C validator