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

Theorem 3eqtrd 2319
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 2315 . 2  |-  ( ph  ->  B  =  D )
51, 4eqtrd 2315 1  |-  ( ph  ->  A  =  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623
This theorem is referenced by:  tpeq123d  3721  oteq123d  3811  resiima  5029  fvun  5589  fvmptd  5606  offval  6085  ofval  6087  onoviun  6360  tz7.44-2  6420  seqomlem4  6465  om1  6540  oe1  6542  oarec  6560  nnm1  6646  cantnff  7375  cantnf0  7376  cantnfp1lem1  7380  cantnfp1lem3  7382  cantnflem3  7393  rankonidlem  7500  rankopb  7524  dfac12lem1  7769  ackbij1lem18  7863  hsmexlem5  8056  axcc3  8064  addpqnq  8562  mulpqnq  8565  mulidnq  8587  recmulnq  8588  prlem934  8657  axrnegex  8784  addid1  8992  cnegex  8993  addcan2  8997  addsub  9062  subsub2  9075  negsubdi2  9106  muladd  9212  mulsub  9222  recextlem1  9398  muleqadd  9412  divrec  9440  div23  9443  div12  9446  divcan7  9469  conjmul  9477  cru  9738  nndivtr  9787  uzindOLD  10106  xnegneg  10541  rexsub  10560  xnegid  10563  xposdif  10582  xmulpnf1  10594  xlemul1  10610  fseq1p1m1  10857  fldiv  10964  zmod10  10987  modcyc  10999  modmul12d  11003  modadd12d  11005  uzrdgsuci  11023  seqeq123d  11055  seqf1olem2  11086  seqid  11091  seqhomo  11093  expneg  11111  expmulz  11148  expdiv  11152  binom3  11222  discr  11238  bcn1  11325  bcnp1n  11326  bcval5  11330  hashbclem  11390  hashf1lem2  11394  ccatlen  11430  swrd0len  11455  ccatswrd  11459  spllen  11469  splfv1  11470  splfv2a  11471  splval2  11472  wrdeqcats1  11474  wrdind  11477  revlen  11480  crim  11600  remullem  11613  remul2  11615  immul2  11622  ipcnval  11628  cjreim  11645  resqrex  11736  sqrneglem  11752  absid  11781  abs1m  11819  sqreulem  11843  amgm2  11853  rlimno1  12127  iseraltlem2  12155  iseraltlem3  12156  iseralt  12157  fsump1i  12232  fsum2dlem  12233  fsumshftm  12243  ackbijnn  12286  binomlem  12287  binom1dif  12291  incexclem  12295  incexc  12296  incexc2  12297  climcndslem2  12309  harmonic  12317  arisum  12318  geo2sum  12329  geo2sum2  12330  cvgrat  12339  mertenslem1  12340  ef0lem  12360  eftlub  12389  efsep  12390  effsumlt  12391  tanval2  12413  efi4p  12417  resin4p  12418  recos4p  12419  tanhlt1  12440  efeul  12442  sinadd  12444  cosadd  12445  sinmul  12452  ef01bndlem  12464  absef  12477  demoivreALT  12481  rpnnen2lem11  12503  dvds2ln  12559  sadcp1  12646  bitsres  12664  smupp1  12671  smupvallem  12674  smueqlem  12681  smumullem  12683  eucalginv  12754  eucalg  12757  zgcdsq  12824  qden1elz  12828  phiprmpw  12844  eulerthlem1  12849  prmdiv  12853  odzdvds  12860  opeo  12866  pythagtriplem12  12879  iserodd  12888  pcqmul  12906  pcaddlem  12936  pcadd  12937  pcadd2  12938  pcmpt  12940  pcmpt2  12941  prmreclem4  12966  prmreclem5  12967  mul4sqlem  13000  4sqlem11  13002  4sqlem17  13008  vdwlem6  13033  vdwlem8  13035  ram0  13069  ramz  13072  ramub1lem2  13074  ramcl  13076  pwsvscafval  13393  sectco  13659  rescabs  13710  cofucl  13762  resf1st  13768  fuccocl  13838  invfuc  13848  homadm  13872  homacd  13873  1stfcl  13971  2ndfcl  13972  prf1st  13978  prf2nd  13979  1st2ndprf  13980  evlfcllem  13995  evlfcl  13996  uncf1  14010  uncf2  14011  curfuncf  14012  diag11  14017  diag12  14018  diag2  14019  hofcllem  14032  hofcl  14033  yon11  14038  yon12  14039  yon2  14040  yonedalem21  14047  yonedalem22  14052  yonedalem3b  14053  yonedainv  14055  latj4rot  14208  cnvps  14321  spwpr4  14340  mhmco  14439  pwsdiagmhm  14445  pwsco1mhm  14446  pwsco2mhm  14447  gsumws1  14462  gsumws2  14465  gsumspl  14466  frmdup2  14487  grpinvid2  14531  grpinvadd  14544  grpsubid1  14551  grpsubadd  14553  grppncan  14556  mulgdirlem  14591  mulgneg2  14594  nmzsubg  14658  divsinv  14676  divssub  14677  conjnmz  14716  gaorber  14762  gastacl  14763  symginv  14782  lactghmga  14784  cntzsubm  14811  gsumwrev  14839  odnncl  14860  odmod  14861  odinv  14874  gexdvdsi  14894  gexdvds  14895  sylow1lem1  14909  sylow2blem3  14933  efgmnvl  15023  efginvrel2  15036  efgsval2  15042  efgsfo  15048  efgredleme  15052  efgredlemd  15053  efgredlemc  15054  efgredlem  15056  frgpinv  15073  vrgpinv  15078  frgpuplem  15081  frgpup1  15084  frgpup2  15085  ablsub2inv  15112  abladdsub4  15115  abladdsub  15116  ablpncan2  15117  ablpnpcan  15121  ablnncan  15122  invghm  15130  gex2abl  15143  gexexlem  15144  oddvdssubg  15147  gsumval3a  15189  gsumzaddlem  15203  gsumzmhm  15210  gsumzinv  15217  gsumsn  15220  gsum2d2lem  15224  dmdprdsplitlem  15272  dprd2db  15278  dpjidcl  15293  ablfac1eulem  15307  ablfac1eu  15308  pgpfac1lem2  15310  pgpfaclem1  15316  ablfaclem2  15321  rngm2neg  15384  dvr1  15471  dvrcan3  15474  abvneg  15599  pwsdiaglmhm  15814  lsppr0  15845  lspsneleq  15868  lspdisj  15878  lspfixed  15881  asclmul1  16079  asclmul2  16080  psrlidm  16148  psrridm  16149  mplsubglem  16179  mpllsslem  16180  mplsubrglem  16183  mplmonmul  16208  mplmon2  16234  mplascl  16237  mplmon2mul  16242  psropprmul  16316  coe1tm  16349  coe1tmfv2  16351  coe1tmmul2  16352  coe1tmmul2fv  16354  coe1pwmulfv  16356  ply1scl0  16365  ply1coe  16368  cnsubrg  16432  ip2di  16545  ip2subdi  16548  ocvlss  16572  lsmcss  16592  ptcld  17307  tgphaus  17799  tgptsmscls  17832  xpsdsval  17945  imasf1oxms  18035  tmsxpsval2  18085  ngptgp  18152  tngnm  18167  nrginvrcnlem  18201  nmoi2  18239  xrsxmet  18315  recld2  18320  reperflem  18323  reconnlem2  18332  phtpycom  18486  pcoass  18522  pi1inv  18550  pi1cof  18557  pi1coghm  18559  nmoleub2lem3  18596  nmoleub3  18600  cphsubrglem  18613  ipcau2  18664  csscld  18676  cmetss  18740  bcth3  18753  pjthlem1  18801  ovolunlem1a  18855  ovolunlem1  18856  ovolicc2lem4  18879  volinun  18903  voliunlem1  18907  volsup  18913  uniioovol  18934  uniioombllem3  18940  uniioombllem4  18941  uniioombllem5  18942  dyadovol  18948  volivth  18962  mbflimsup  19021  i1faddlem  19048  itg1addlem4  19054  itg1addlem5  19055  mbfi1fseqlem6  19075  itg2const2  19096  itgcnlem  19144  itgrevallem1  19149  itgposval  19150  itgitg1  19163  itgaddlem2  19178  iblmulc2  19185  itgmulc2lem2  19187  itgmulc2  19188  itgabs  19189  itgspliticc  19191  ditgsplit  19211  dvcmul  19293  dvcobr  19295  dvexp  19302  dvmptres2  19311  dvmptcmul  19313  dvexp3  19325  dvlip2  19342  dv11cn  19348  lhop1lem  19360  dvfsumlem2  19374  ftc1lem4  19386  ftc2  19391  ftc2ditg  19393  itgparts  19394  itgsubstlem  19395  evlslem3  19398  evlslem1  19399  evl1sca  19413  evl1var  19415  evl1addd  19417  evl1subd  19418  evl1muld  19419  pf1mpf  19435  tdeglem4  19446  mdegvscale  19461  mdegmullem  19464  coe1mul3  19485  deg1add  19489  deg1sublt  19496  deg1mul3le  19502  uc1pmon1p  19537  ply1remlem  19548  ply1rem  19549  fta1glem2  19552  fta1g  19553  plypf1  19594  dgradd2  19649  dgrmulc  19652  dgrcolem2  19655  dvply1  19664  plydivlem4  19676  fta1lem  19687  vieta1lem1  19690  vieta1lem2  19691  vieta1  19692  aareccl  19706  geolim3  19719  aaliou2b  19721  tayl0  19741  taylply2  19747  taylthlem1  19752  ulmshft  19769  radcnv0  19792  dvradcnv  19797  pserulm  19798  psercn  19802  pserdvlem2  19804  pserdv  19805  abelthlem7  19814  abelth  19817  ef2kpi  19846  sinhalfpip  19860  sinhalfpim  19861  coshalfpim  19863  ptolemy  19864  tangtx  19873  tanabsge  19874  pige3  19885  sineq0  19889  resinf1o  19898  tanregt0  19901  efif1olem2  19905  efif1olem4  19907  eff1olem  19910  logrnaddcl  19931  logneg  19941  eflogeq  19955  cosargd  19962  logimul  19968  logneg2  19969  tanarg  19970  logcnlem4  19992  logcn  19994  advlogexp  20002  logtayl  20007  cxpsqrlem  20049  cxpsqr  20050  dvcxp1  20082  dvcxp2  20083  cxpcn3  20088  sqrcn  20090  abscxpbnd  20093  root1cj  20096  cxpeq  20097  cosangneg2d  20105  ang180lem1  20107  lawcos  20114  pythag  20115  isosctrlem2  20119  isosctrlem3  20120  chordthmlem4  20132  dcubic1lem  20139  dcubic2  20140  dcubic1  20141  dcubic  20142  mcubic  20143  cubic2  20144  binom4  20146  dquartlem1  20147  dquartlem2  20148  dquart  20149  quart1lem  20151  quart1  20152  quartlem1  20153  asinlem2  20165  asinneg  20182  sinasin  20185  cosacos  20186  asinsinlem  20187  asinsin  20188  cosasin  20200  atancj  20206  efiatan  20208  atanlogsublem  20211  efiatan2  20213  2efiatan  20214  cosatan  20217  atantan  20219  dvatan  20231  atantayl  20233  atantayl2  20234  log2cnv  20240  log2tlbnd  20241  rlimcnp  20260  efrlim  20264  cxp2limlem  20270  jensen  20283  amgmlem  20284  amgm  20285  emcllem5  20293  wilthlem1  20306  wilthlem2  20307  ftalem5  20314  basellem2  20319  basellem3  20320  basellem4  20321  basellem5  20322  basellem8  20325  vmappw  20354  0sgm  20382  chtprm  20391  ppidif  20401  fsumdvdscom  20425  muinv  20433  fsumdvdsmul  20435  sgmppw  20436  0sgmppw  20437  1sgm2ppw  20439  chtublem  20450  chtub  20451  vmasum  20455  logfac2  20456  chpval2  20457  logfacrlim  20463  logexprlim  20464  perfectlem2  20469  perfect  20470  dchrsum2  20507  dchr2sum  20512  sum2dchr  20513  bposlem5  20527  bposlem9  20531  lgsval2lem  20545  lgsval4  20555  lgsval4a  20557  lgsneg  20558  lgsneg1  20559  lgsdir  20569  lgsne0  20572  lgsqrlem1  20580  lgseisenlem3  20590  lgseisenlem4  20591  lgsquadlem1  20593  lgsquadlem2  20594  lgsquad2lem1  20597  2sqlem3  20605  2sqblem  20616  chebbnd1lem1  20618  chebbnd1lem2  20619  chebbnd1  20621  rplogsumlem1  20633  rplogsumlem2  20634  rpvmasumlem  20636  dchrisumlem1  20638  dchrvmasumlem1  20644  dchrvmasumiflem1  20650  dchrvmasumiflem2  20651  dchrisum0flblem1  20657  rpvmasum2  20661  dchrisum0re  20662  rplogsum  20676  mudivsum  20679  mulogsum  20681  mulog2sumlem1  20683  mulog2sumlem2  20684  vmalogdivsum  20688  logsqvma  20691  selberg  20697  selberg2lem  20699  selberg2  20700  selberg3lem1  20706  selberg4lem1  20709  selberg4  20710  pntrmax  20713  pntrsumo1  20714  selbergr  20717  selberg34r  20720  pntsval2  20725  pntrlog2bndlem2  20727  pntrlog2bndlem4  20729  pntrlog2bndlem5  20730  pntpbnd1a  20734  pntpbnd2  20736  pntibndlem2  20740  pntlemb  20746  pntlemn  20749  pntlemr  20751  pntlemj  20752  pntlemf  20754  pntlemo  20756  pnt2  20762  ostth2  20786  ostth3  20787  grpoinvid2  20898  grpoasscan2  20905  grpoinvop  20908  grpoinvdiv  20912  grpopncan  20918  grpopnpcan2  20920  gxpval  20926  gxnval  20927  gxmul  20945  gxmodid  20946  ablomuldiv  20956  ablonncan  20961  gxdi  20963  ablomul  21022  vcnegsubdi2  21131  vcoprne  21135  nvnegneg  21209  nvsubadd  21213  nvnncan  21221  nvdif  21231  nvpi  21232  nvabs  21239  nvge0  21240  nvnd  21257  imsmetlem  21259  dipcj  21290  0lno  21368  blocnilem  21382  ipasslem4  21412  ipasslem5  21413  ubthlem2  21450  htthlem  21497  hvpncan  21618  hvaddsub4  21657  his5  21665  his2sub  21671  bcsiALT  21758  norm1  21828  hhssmetdval  21855  pjhthlem1  21970  pjspansn  22156  cm2j  22199  5oalem2  22234  3oalem2  22242  mayete3i  22307  mayete3iOLD  22308  hoaddid1i  22366  honegsubdi2  22391  hoaddsub  22396  unoplin  22500  counop  22501  hmoplin  22522  hmopco  22603  riesz3i  22642  cnlnadjlem7  22653  adjcoi  22680  kbass2  22697  kbass6  22701  opsqrlem1  22720  hmopidmpji  22732  pjssposi  22752  pjclem4  22779  strlem1  22830  chirredlem2  22971  ballotlemfp1  23050  xdivrec  23110  iuninc  23158  fimacnvinrn  23199  fmptpr  23214  xaddeq0  23304  xrsinvgval  23306  xrge0iifhom  23319  xrge0iif1  23320  xrge0npcan  23333  gsumsn2  23378  logbrec  23407  esumsn  23437  esumpr  23438  esumpinfval  23441  esumpinfsum  23445  esummulc2  23450  hasheuni  23453  cndprobtot  23639  cndprobnul  23640  orvcval2  23659  dstrvval  23671  dstrvprob  23672  zetacvg  23689  subfacp1lem5  23715  subfacp1lem6  23716  subfacval2  23718  subfaclim  23719  txsconlem  23771  cvxscon  23774  cvmliftlem5  23820  cvmliftlem10  23825  cvmliftlem11  23826  cvmliftlem13  23827  cvmlift2lem12  23845  cvmliftphtlem  23848  ghomf1olem  24001  modaddabs  24011  gcdabsorb  24105  brbtwn2  24533  colinearalglem1  24534  colinearalglem4  24537  axsegconlem9  24553  ax5seglem2  24557  axeuclidlem  24590  axcontlem7  24598  linethru  24776  bpolylem  24783  bpolysum  24788  bpolydiflem  24789  bpoly2  24792  bpoly3  24793  bpoly4  24794  fsumcube  24795  areacirclem2  24925  areacirc  24931  imfstnrelc  25081  mapex2  25140  sege  25252  ubos  25256  toplat  25290  prodeq123d  25316  fprod1i  25322  reacomsmgrp1  25343  reacomsmgrp2  25344  reacomsmgrp3  25345  resgcom  25351  caytr  25400  ltrran2  25403  ltrooo  25404  ltrinvlem  25406  rltrran  25414  multinv  25422  mult2inv  25424  dblsubvec  25474  muldisc  25481  svli2  25484  sallnei  25529  usptop  25550  islimrs  25580  2wsms  25608  valvze  25654  addassv  25656  isdivcv2  25693  isder  25707  1cat  25759  isfuna  25834  idsubfun  25858  grphidmor  25952  cmp2morpgrp  25963  cmp2morpdom  25964  cmpmorass  25966  isconc3  26008  lineval222  26079  lineval3a  26083  sgplpte22  26138  isside0  26164  bosser  26167  aishp  26172  upixp  26403  fdc  26455  heiborlem4  26538  heiborlem6  26540  iscringd  26624  keridl  26657  fninfp  26754  fndifnfp  26756  lcomfsup  26768  diophrw  26838  eldioph2lem1  26839  irrapxlem3  26909  irrapxlem5  26911  pellexlem2  26915  pellexlem6  26919  pell1234qrmulcl  26940  pell14qrgt0  26944  pell1234qrdich  26946  reglogexpbas  26982  rmxy1  27007  rmxy0  27008  rmym1  27020  rmxluc  27021  rmyluc  27022  rmxdbl  27024  rmydbl  27025  jm2.18  27081  jm2.19lem4  27085  jm2.22  27088  jm2.23  27089  jm2.25  27092  jm2.27c  27100  jm3.1lem2  27111  lmhmfgsplit  27184  dsmmsubg  27209  frlmvscaval  27231  frlmssuvc2  27247  frlmsslsp  27248  frlmup1  27250  frlmup2  27251  enfixsn  27257  islindf4  27308  indlcim  27310  hbtlem1  27327  dgrsub2  27339  mpaaeu  27355  rgspnval  27373  rngunsnply  27378  pmtrmvd  27398  symggen  27411  symgtrinv  27413  psgnunilem5  27417  psgnunilem2  27418  psgnunilem4  27420  mamulid  27458  mamurid  27459  matbas2  27475  hashgcdlem  27516  proot1hash  27519  proot1ex  27520  m1expeven  27725  clim1fr1  27727  climexp  27731  climneg  27736  climdivf  27738  stoweidlem10  27759  stoweidlem11  27760  stoweidlem22  27771  wallispilem4  27817  wallispilem5  27818  wallispi  27819  wallispi2lem1  27820  wallispi2lem2  27821  wallispi2  27822  stirlinglem1  27823  stirlinglem3  27825  stirlinglem4  27826  stirlinglem5  27827  stirlinglem6  27828  stirlinglem7  27829  stirlinglem10  27832  stirlinglem14  27836  stirlinglem15  27837  sigarac  27842  sigaras  27845  sigarms  27846  sigarexp  27849  sigarperm  27850  sigarcol  27854  sharhght  27855  sigaradd  27856  cevathlem2  27858  afvres  28034  difprsneq  28068  difprsng  28069  diftpsneq  28070  s2prop  28089  s4prop  28090  uvtxnm1nbgra  28166  sinh-conventional  28209  sgnp  28247  sgnn  28251  lsmsat  29198  lflsub  29257  lfladdcl  29261  lflvscl  29267  lkrlss  29285  eqlkr  29289  lkrlsp  29292  ldualvsdi1  29333  ldualvsdi2  29334  ldualgrplem  29335  ldualvsubval  29347  lkrin  29354  latmassOLD  29419  omlfh1N  29448  glbconN  29566  3atlem2  29673  lplnexllnN  29753  dalem24  29886  pmapat  29952  pmapmeet  29962  atmod4i1  30055  atmod4i2  30056  pol1N  30099  2polpmapN  30102  2polvalN  30103  poldmj1N  30117  polatN  30120  osumcllem3N  30147  lhpmcvr3  30214  ldilco  30305  trl0  30359  cdlemc1  30380  cdlemc6  30385  cdleme0cp  30403  cdleme0cq  30404  cdleme1  30416  cdleme4  30427  cdleme8  30439  cdleme9  30442  cdleme10  30443  cdleme11g  30454  cdleme20j  30507  cdleme22e  30533  cdleme22eALTN  30534  cdleme23b  30539  cdleme30a  30567  cdlemefrs32fva  30589  cdleme35b  30639  cdleme35e  30642  cdleme17d2  30684  cdleme48d  30724  cdlemg4  30806  cdlemg7aN  30814  cdlemg17f  30855  trlcoabs2N  30911  trlcolem  30915  tendo0pl  30980  erngset  30989  erngset-rN  30997  cdlemh1  31004  cdlemi1  31007  cdlemk20  31063  cdlemk40  31106  cdlemkid1  31111  cdlemkfid3N  31114  erngdvlem3  31179  erngdvlem4  31180  erngdvlem3-rN  31187  tendocnv  31211  dia0  31242  diameetN  31246  dia2dimlem3  31256  dia2dimlem4  31257  cdlemn3  31387  cdlemn9  31395  dihordlem7b  31405  dih1  31476  dihwN  31479  dihglbcpreN  31490  dihmeetcN  31492  dihmeetbclemN  31494  dihmeetlem4preN  31496  dihmeetlem13N  31509  dihmeet  31533  doch1  31549  doch2val2  31554  dihoml4c  31566  djhexmid  31601  djh01  31602  dihjat1  31619  lclkrlem2c  31699  lclkrlem2j  31706  lclkrlem2m  31709  lcfrlem1  31732  lcfrlem23  31755  lcd0v  31801  lcdvsubval  31808  mapdindp  31861  mapdpglem21  31882  baerlem5alem1  31898  baerlem5blem1  31899  baerlem5amN  31906  baerlem5bmN  31907  baerlem5abmN  31908  hdmap10  32033  hdmapsub  32040  hdmaprnlem6N  32047  hdmap14lem8  32068  hgmapmul  32088  hdmapinvlem3  32113  hdmapinvlem4  32114  hgmapvvlem1  32116  hdmapglem7b  32121
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276
  Copyright terms: Public domain W3C validator