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

Theorem 3eqtrd 2332
Description: A deduction from three chained equalities. (Contributed by NM, 29-Oct-1995.)
Hypotheses
Ref Expression
3eqtrd.1  |-  ( ph  ->  A  =  B )
3eqtrd.2  |-  ( ph  ->  B  =  C )
3eqtrd.3  |-  ( ph  ->  C  =  D )
Assertion
Ref Expression
3eqtrd  |-  ( ph  ->  A  =  D )

Proof of Theorem 3eqtrd
StepHypRef Expression
1 3eqtrd.1 . 2  |-  ( ph  ->  A  =  B )
2 3eqtrd.2 . . 3  |-  ( ph  ->  B  =  C )
3 3eqtrd.3 . . 3  |-  ( ph  ->  C  =  D )
42, 3eqtrd 2328 . 2  |-  ( ph  ->  B  =  D )
51, 4eqtrd 2328 1  |-  ( ph  ->  A  =  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632
This theorem is referenced by:  tpeq123d  3734  diftpsn3  3772  oteq123d  3827  resiima  5045  fvun  5605  fvmptd  5622  offval  6101  ofval  6103  onoviun  6376  tz7.44-2  6436  seqomlem4  6481  om1  6556  oe1  6558  oarec  6576  nnm1  6662  cantnff  7391  cantnf0  7392  cantnfp1lem1  7396  cantnfp1lem3  7398  cantnflem3  7409  rankonidlem  7516  rankopb  7540  dfac12lem1  7785  ackbij1lem18  7879  hsmexlem5  8072  axcc3  8080  addpqnq  8578  mulpqnq  8581  mulidnq  8603  recmulnq  8604  prlem934  8673  axrnegex  8800  addid1  9008  cnegex  9009  addcan2  9013  addsub  9078  subsub2  9091  negsubdi2  9122  muladd  9228  mulsub  9238  recextlem1  9414  muleqadd  9428  divrec  9456  div23  9459  div12  9462  divcan7  9485  conjmul  9493  cru  9754  nndivtr  9803  uzindOLD  10122  xnegneg  10557  rexsub  10576  xnegid  10579  xposdif  10598  xmulpnf1  10610  xlemul1  10626  fseq1p1m1  10873  fldiv  10980  zmod10  11003  modcyc  11015  modmul12d  11019  modadd12d  11021  uzrdgsuci  11039  seqeq123d  11071  seqf1olem2  11102  seqid  11107  seqhomo  11109  expneg  11127  expmulz  11164  expdiv  11168  binom3  11238  discr  11254  bcn1  11341  bcnp1n  11342  bcval5  11346  hashbclem  11406  hashf1lem2  11410  ccatlen  11446  swrd0len  11471  ccatswrd  11475  spllen  11485  splfv1  11486  splfv2a  11487  splval2  11488  wrdeqcats1  11490  wrdind  11493  revlen  11496  crim  11616  remullem  11629  remul2  11631  immul2  11638  ipcnval  11644  cjreim  11661  resqrex  11752  sqrneglem  11768  absid  11797  abs1m  11835  sqreulem  11859  amgm2  11869  rlimno1  12143  iseraltlem2  12171  iseraltlem3  12172  iseralt  12173  fsump1i  12248  fsum2dlem  12249  fsumshftm  12259  ackbijnn  12302  binomlem  12303  binom1dif  12307  incexclem  12311  incexc  12312  incexc2  12313  climcndslem2  12325  harmonic  12333  arisum  12334  geo2sum  12345  geo2sum2  12346  cvgrat  12355  mertenslem1  12356  ef0lem  12376  eftlub  12405  efsep  12406  effsumlt  12407  tanval2  12429  efi4p  12433  resin4p  12434  recos4p  12435  tanhlt1  12456  efeul  12458  sinadd  12460  cosadd  12461  sinmul  12468  ef01bndlem  12480  absef  12493  demoivreALT  12497  rpnnen2lem11  12519  dvds2ln  12575  sadcp1  12662  bitsres  12680  smupp1  12687  smupvallem  12690  smueqlem  12697  smumullem  12699  eucalginv  12770  eucalg  12773  zgcdsq  12840  qden1elz  12844  phiprmpw  12860  eulerthlem1  12865  prmdiv  12869  odzdvds  12876  opeo  12882  pythagtriplem12  12895  iserodd  12904  pcqmul  12922  pcaddlem  12952  pcadd  12953  pcadd2  12954  pcmpt  12956  pcmpt2  12957  prmreclem4  12982  prmreclem5  12983  mul4sqlem  13016  4sqlem11  13018  4sqlem17  13024  vdwlem6  13049  vdwlem8  13051  ram0  13085  ramz  13088  ramub1lem2  13090  ramcl  13092  pwsvscafval  13409  sectco  13675  rescabs  13726  cofucl  13778  resf1st  13784  fuccocl  13854  invfuc  13864  homadm  13888  homacd  13889  1stfcl  13987  2ndfcl  13988  prf1st  13994  prf2nd  13995  1st2ndprf  13996  evlfcllem  14011  evlfcl  14012  uncf1  14026  uncf2  14027  curfuncf  14028  diag11  14033  diag12  14034  diag2  14035  hofcllem  14048  hofcl  14049  yon11  14054  yon12  14055  yon2  14056  yonedalem21  14063  yonedalem22  14068  yonedalem3b  14069  yonedainv  14071  latj4rot  14224  cnvps  14337  spwpr4  14356  mhmco  14455  pwsdiagmhm  14461  pwsco1mhm  14462  pwsco2mhm  14463  gsumws1  14478  gsumws2  14481  gsumspl  14482  frmdup2  14503  grpinvid2  14547  grpinvadd  14560  grpsubid1  14567  grpsubadd  14569  grppncan  14572  mulgdirlem  14607  mulgneg2  14610  nmzsubg  14674  divsinv  14692  divssub  14693  conjnmz  14732  gaorber  14778  gastacl  14779  symginv  14798  lactghmga  14800  cntzsubm  14827  gsumwrev  14855  odnncl  14876  odmod  14877  odinv  14890  gexdvdsi  14910  gexdvds  14911  sylow1lem1  14925  sylow2blem3  14949  efgmnvl  15039  efginvrel2  15052  efgsval2  15058  efgsfo  15064  efgredleme  15068  efgredlemd  15069  efgredlemc  15070  efgredlem  15072  frgpinv  15089  vrgpinv  15094  frgpuplem  15097  frgpup1  15100  frgpup2  15101  ablsub2inv  15128  abladdsub4  15131  abladdsub  15132  ablpncan2  15133  ablpnpcan  15137  ablnncan  15138  invghm  15146  gex2abl  15159  gexexlem  15160  oddvdssubg  15163  gsumval3a  15205  gsumzaddlem  15219  gsumzmhm  15226  gsumzinv  15233  gsumsn  15236  gsum2d2lem  15240  dmdprdsplitlem  15288  dprd2db  15294  dpjidcl  15309  ablfac1eulem  15323  ablfac1eu  15324  pgpfac1lem2  15326  pgpfaclem1  15332  ablfaclem2  15337  rngm2neg  15400  dvr1  15487  dvrcan3  15490  abvneg  15615  pwsdiaglmhm  15830  lsppr0  15861  lspsneleq  15884  lspdisj  15894  lspfixed  15897  asclmul1  16095  asclmul2  16096  psrlidm  16164  psrridm  16165  mplsubglem  16195  mpllsslem  16196  mplsubrglem  16199  mplmonmul  16224  mplmon2  16250  mplascl  16253  mplmon2mul  16258  psropprmul  16332  coe1tm  16365  coe1tmfv2  16367  coe1tmmul2  16368  coe1tmmul2fv  16370  coe1pwmulfv  16372  ply1scl0  16381  ply1coe  16384  cnsubrg  16448  ip2di  16561  ip2subdi  16564  ocvlss  16588  lsmcss  16608  ptcld  17323  tgphaus  17815  tgptsmscls  17848  xpsdsval  17961  imasf1oxms  18051  tmsxpsval2  18101  ngptgp  18168  tngnm  18183  nrginvrcnlem  18217  nmoi2  18255  xrsxmet  18331  recld2  18336  reperflem  18339  reconnlem2  18348  phtpycom  18502  pcoass  18538  pi1inv  18566  pi1cof  18573  pi1coghm  18575  nmoleub2lem3  18612  nmoleub3  18616  cphsubrglem  18629  ipcau2  18680  csscld  18692  cmetss  18756  bcth3  18769  pjthlem1  18817  ovolunlem1a  18871  ovolunlem1  18872  ovolicc2lem4  18895  volinun  18919  voliunlem1  18923  volsup  18929  uniioovol  18950  uniioombllem3  18956  uniioombllem4  18957  uniioombllem5  18958  dyadovol  18964  volivth  18978  mbflimsup  19037  i1faddlem  19064  itg1addlem4  19070  itg1addlem5  19071  mbfi1fseqlem6  19091  itg2const2  19112  itgcnlem  19160  itgrevallem1  19165  itgposval  19166  itgitg1  19179  itgaddlem2  19194  iblmulc2  19201  itgmulc2lem2  19203  itgmulc2  19204  itgabs  19205  itgspliticc  19207  ditgsplit  19227  dvcmul  19309  dvcobr  19311  dvexp  19318  dvmptres2  19327  dvmptcmul  19329  dvexp3  19341  dvlip2  19358  dv11cn  19364  lhop1lem  19376  dvfsumlem2  19390  ftc1lem4  19402  ftc2  19407  ftc2ditg  19409  itgparts  19410  itgsubstlem  19411  evlslem3  19414  evlslem1  19415  evl1sca  19429  evl1var  19431  evl1addd  19433  evl1subd  19434  evl1muld  19435  pf1mpf  19451  tdeglem4  19462  mdegvscale  19477  mdegmullem  19480  coe1mul3  19501  deg1add  19505  deg1sublt  19512  deg1mul3le  19518  uc1pmon1p  19553  ply1remlem  19564  ply1rem  19565  fta1glem2  19568  fta1g  19569  plypf1  19610  dgradd2  19665  dgrmulc  19668  dgrcolem2  19671  dvply1  19680  plydivlem4  19692  fta1lem  19703  vieta1lem1  19706  vieta1lem2  19707  vieta1  19708  aareccl  19722  geolim3  19735  aaliou2b  19737  tayl0  19757  taylply2  19763  taylthlem1  19768  ulmshft  19785  radcnv0  19808  dvradcnv  19813  pserulm  19814  psercn  19818  pserdvlem2  19820  pserdv  19821  abelthlem7  19830  abelth  19833  ef2kpi  19862  sinhalfpip  19876  sinhalfpim  19877  coshalfpim  19879  ptolemy  19880  tangtx  19889  tanabsge  19890  pige3  19901  sineq0  19905  resinf1o  19914  tanregt0  19917  efif1olem2  19921  efif1olem4  19923  eff1olem  19926  logrnaddcl  19947  logneg  19957  eflogeq  19971  cosargd  19978  logimul  19984  logneg2  19985  tanarg  19986  logcnlem4  20008  logcn  20010  advlogexp  20018  logtayl  20023  cxpsqrlem  20065  cxpsqr  20066  dvcxp1  20098  dvcxp2  20099  cxpcn3  20104  sqrcn  20106  abscxpbnd  20109  root1cj  20112  cxpeq  20113  cosangneg2d  20121  ang180lem1  20123  lawcos  20130  pythag  20131  isosctrlem2  20135  isosctrlem3  20136  chordthmlem4  20148  dcubic1lem  20155  dcubic2  20156  dcubic1  20157  dcubic  20158  mcubic  20159  cubic2  20160  binom4  20162  dquartlem1  20163  dquartlem2  20164  dquart  20165  quart1lem  20167  quart1  20168  quartlem1  20169  asinlem2  20181  asinneg  20198  sinasin  20201  cosacos  20202  asinsinlem  20203  asinsin  20204  cosasin  20216  atancj  20222  efiatan  20224  atanlogsublem  20227  efiatan2  20229  2efiatan  20230  cosatan  20233  atantan  20235  dvatan  20247  atantayl  20249  atantayl2  20250  log2cnv  20256  log2tlbnd  20257  rlimcnp  20276  efrlim  20280  cxp2limlem  20286  jensen  20299  amgmlem  20300  amgm  20301  emcllem5  20309  wilthlem1  20322  wilthlem2  20323  ftalem5  20330  basellem2  20335  basellem3  20336  basellem4  20337  basellem5  20338  basellem8  20341  vmappw  20370  0sgm  20398  chtprm  20407  ppidif  20417  fsumdvdscom  20441  muinv  20449  fsumdvdsmul  20451  sgmppw  20452  0sgmppw  20453  1sgm2ppw  20455  chtublem  20466  chtub  20467  vmasum  20471  logfac2  20472  chpval2  20473  logfacrlim  20479  logexprlim  20480  perfectlem2  20485  perfect  20486  dchrsum2  20523  dchr2sum  20528  sum2dchr  20529  bposlem5  20543  bposlem9  20547  lgsval2lem  20561  lgsval4  20571  lgsval4a  20573  lgsneg  20574  lgsneg1  20575  lgsdir  20585  lgsne0  20588  lgsqrlem1  20596  lgseisenlem3  20606  lgseisenlem4  20607  lgsquadlem1  20609  lgsquadlem2  20610  lgsquad2lem1  20613  2sqlem3  20621  2sqblem  20632  chebbnd1lem1  20634  chebbnd1lem2  20635  chebbnd1  20637  rplogsumlem1  20649  rplogsumlem2  20650  rpvmasumlem  20652  dchrisumlem1  20654  dchrvmasumlem1  20660  dchrvmasumiflem1  20666  dchrvmasumiflem2  20667  dchrisum0flblem1  20673  rpvmasum2  20677  dchrisum0re  20678  rplogsum  20692  mudivsum  20695  mulogsum  20697  mulog2sumlem1  20699  mulog2sumlem2  20700  vmalogdivsum  20704  logsqvma  20707  selberg  20713  selberg2lem  20715  selberg2  20716  selberg3lem1  20722  selberg4lem1  20725  selberg4  20726  pntrmax  20729  pntrsumo1  20730  selbergr  20733  selberg34r  20736  pntsval2  20741  pntrlog2bndlem2  20743  pntrlog2bndlem4  20745  pntrlog2bndlem5  20746  pntpbnd1a  20750  pntpbnd2  20752  pntibndlem2  20756  pntlemb  20762  pntlemn  20765  pntlemr  20767  pntlemj  20768  pntlemf  20770  pntlemo  20772  pnt2  20778  ostth2  20802  ostth3  20803  grpoinvid2  20914  grpoasscan2  20921  grpoinvop  20924  grpoinvdiv  20928  grpopncan  20934  grpopnpcan2  20936  gxpval  20942  gxnval  20943  gxmul  20961  gxmodid  20962  ablomuldiv  20972  ablonncan  20977  gxdi  20979  ablomul  21038  vcnegsubdi2  21147  vcoprne  21151  nvnegneg  21225  nvsubadd  21229  nvnncan  21237  nvdif  21247  nvpi  21248  nvabs  21255  nvge0  21256  nvnd  21273  imsmetlem  21275  dipcj  21306  0lno  21384  blocnilem  21398  ipasslem4  21428  ipasslem5  21429  ubthlem2  21466  htthlem  21513  hvpncan  21634  hvaddsub4  21673  his5  21681  his2sub  21687  bcsiALT  21774  norm1  21844  hhssmetdval  21871  pjhthlem1  21986  pjspansn  22172  cm2j  22215  5oalem2  22250  3oalem2  22258  mayete3i  22323  mayete3iOLD  22324  hoaddid1i  22382  honegsubdi2  22407  hoaddsub  22412  unoplin  22516  counop  22517  hmoplin  22538  hmopco  22619  riesz3i  22658  cnlnadjlem7  22669  adjcoi  22696  kbass2  22713  kbass6  22717  opsqrlem1  22736  hmopidmpji  22748  pjssposi  22768  pjclem4  22795  strlem1  22846  chirredlem2  22987  ballotlemfp1  23066  xdivrec  23126  iuninc  23174  fimacnvinrn  23214  fmptpr  23229  xaddeq0  23319  xrsinvgval  23321  xrge0iifhom  23334  xrge0iif1  23335  xrge0npcan  23348  gsumsn2  23393  logbrec  23422  esumsn  23452  esumpr  23453  esumpinfval  23456  esumpinfsum  23460  esummulc2  23465  hasheuni  23468  cndprobtot  23654  cndprobnul  23655  orvcval2  23674  dstrvval  23686  dstrvprob  23687  zetacvg  23704  subfacp1lem5  23730  subfacp1lem6  23731  subfacval2  23733  subfaclim  23734  txsconlem  23786  cvxscon  23789  cvmliftlem5  23835  cvmliftlem10  23840  cvmliftlem11  23841  cvmliftlem13  23842  cvmlift2lem12  23860  cvmliftphtlem  23863  ghomf1olem  24016  modaddabs  24026  faclimlem5  24121  faclimlem9  24125  gcdabsorb  24176  brbtwn2  24605  colinearalglem1  24606  colinearalglem4  24609  axsegconlem9  24625  ax5seglem2  24629  axeuclidlem  24662  axcontlem7  24670  linethru  24848  bpolylem  24855  bpolysum  24860  bpolydiflem  24861  bpoly2  24864  bpoly3  24865  bpoly4  24866  fsumcube  24867  itg2addnclem  25003  itg2addnclem2  25004  itgaddnclem2  25010  iblmulc2nc  25016  itgmulc2nclem2  25018  itgmulc2nc  25019  itgabsnc  25020  ftc1cnnclem  25024  areacirclem2  25028  areacirc  25034  imfstnrelc  25184  mapex2  25243  sege  25355  ubos  25359  toplat  25393  prodeq123d  25419  fprod1i  25425  reacomsmgrp1  25446  reacomsmgrp2  25447  reacomsmgrp3  25448  resgcom  25454  caytr  25503  ltrran2  25506  ltrooo  25507  ltrinvlem  25509  rltrran  25517  multinv  25525  mult2inv  25527  dblsubvec  25577  muldisc  25584  svli2  25587  sallnei  25632  usptop  25653  islimrs  25683  2wsms  25711  valvze  25757  addassv  25759  isdivcv2  25796  isder  25810  1cat  25862  isfuna  25937  idsubfun  25961  grphidmor  26055  cmp2morpgrp  26066  cmp2morpdom  26067  cmpmorass  26069  isconc3  26111  lineval222  26182  lineval3a  26186  sgplpte22  26241  isside0  26267  bosser  26270  aishp  26275  upixp  26506  fdc  26558  heiborlem4  26641  heiborlem6  26643  iscringd  26727  keridl  26760  fninfp  26857  fndifnfp  26859  lcomfsup  26871  diophrw  26941  eldioph2lem1  26942  irrapxlem3  27012  irrapxlem5  27014  pellexlem2  27018  pellexlem6  27022  pell1234qrmulcl  27043  pell14qrgt0  27047  pell1234qrdich  27049  reglogexpbas  27085  rmxy1  27110  rmxy0  27111  rmym1  27123  rmxluc  27124  rmyluc  27125  rmxdbl  27127  rmydbl  27128  jm2.18  27184  jm2.19lem4  27188  jm2.22  27191  jm2.23  27192  jm2.25  27195  jm2.27c  27203  jm3.1lem2  27214  lmhmfgsplit  27287  dsmmsubg  27312  frlmvscaval  27334  frlmssuvc2  27350  frlmsslsp  27351  frlmup1  27353  frlmup2  27354  enfixsn  27360  islindf4  27411  indlcim  27413  hbtlem1  27430  dgrsub2  27442  mpaaeu  27458  rgspnval  27476  rngunsnply  27481  pmtrmvd  27501  symggen  27514  symgtrinv  27516  psgnunilem5  27520  psgnunilem2  27521  psgnunilem4  27523  mamulid  27561  mamurid  27562  matbas2  27578  hashgcdlem  27619  proot1hash  27622  proot1ex  27623  m1expeven  27828  clim1fr1  27830  climexp  27834  climneg  27839  climdivf  27841  stoweidlem10  27862  stoweidlem11  27863  stoweidlem22  27874  wallispilem4  27920  wallispilem5  27921  wallispi  27922  wallispi2lem1  27923  wallispi2lem2  27924  wallispi2  27925  stirlinglem1  27926  stirlinglem3  27928  stirlinglem4  27929  stirlinglem5  27930  stirlinglem6  27931  stirlinglem7  27932  stirlinglem10  27935  stirlinglem14  27939  stirlinglem15  27940  sigarac  27945  sigaras  27948  sigarms  27949  sigarexp  27952  sigarperm  27953  sigarcol  27957  sharhght  27958  sigaradd  27959  cevathlem2  27961  afvres  28140  s2prop  28221  s4prop  28222  uvtxnm1nbgra  28307  sinh-conventional  28463  sgnp  28501  sgnn  28505  lsmsat  29820  lflsub  29879  lfladdcl  29883  lflvscl  29889  lkrlss  29907  eqlkr  29911  lkrlsp  29914  ldualvsdi1  29955  ldualvsdi2  29956  ldualgrplem  29957  ldualvsubval  29969  lkrin  29976  latmassOLD  30041  omlfh1N  30070  glbconN  30188  3atlem2  30295  lplnexllnN  30375  dalem24  30508  pmapat  30574  pmapmeet  30584  atmod4i1  30677  atmod4i2  30678  pol1N  30721  2polpmapN  30724  2polvalN  30725  poldmj1N  30739  polatN  30742  osumcllem3N  30769  lhpmcvr3  30836  ldilco  30927  trl0  30981  cdlemc1  31002  cdlemc6  31007  cdleme0cp  31025  cdleme0cq  31026  cdleme1  31038  cdleme4  31049  cdleme8  31061  cdleme9  31064  cdleme10  31065  cdleme11g  31076  cdleme20j  31129  cdleme22e  31155  cdleme22eALTN  31156  cdleme23b  31161  cdleme30a  31189  cdlemefrs32fva  31211  cdleme35b  31261  cdleme35e  31264  cdleme17d2  31306  cdleme48d  31346  cdlemg4  31428  cdlemg7aN  31436  cdlemg17f  31477  trlcoabs2N  31533  trlcolem  31537  tendo0pl  31602  erngset  31611  erngset-rN  31619  cdlemh1  31626  cdlemi1  31629  cdlemk20  31685  cdlemk40  31728  cdlemkid1  31733  cdlemkfid3N  31736  erngdvlem3  31801  erngdvlem4  31802  erngdvlem3-rN  31809  tendocnv  31833  dia0  31864  diameetN  31868  dia2dimlem3  31878  dia2dimlem4  31879  cdlemn3  32009  cdlemn9  32017  dihordlem7b  32027  dih1  32098  dihwN  32101  dihglbcpreN  32112  dihmeetcN  32114  dihmeetbclemN  32116  dihmeetlem4preN  32118  dihmeetlem13N  32131  dihmeet  32155  doch1  32171  doch2val2  32176  dihoml4c  32188  djhexmid  32223  djh01  32224  dihjat1  32241  lclkrlem2c  32321  lclkrlem2j  32328  lclkrlem2m  32331  lcfrlem1  32354  lcfrlem23  32377  lcd0v  32423  lcdvsubval  32430  mapdindp  32483  mapdpglem21  32504  baerlem5alem1  32520  baerlem5blem1  32521  baerlem5amN  32528  baerlem5bmN  32529  baerlem5abmN  32530  hdmap10  32655  hdmapsub  32662  hdmaprnlem6N  32669  hdmap14lem8  32690  hgmapmul  32710  hdmapinvlem3  32735  hdmapinvlem4  32736  hgmapvvlem1  32738  hdmapglem7b  32743
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