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

Theorem 3eqtr3d 2516
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 2510 . 2  |-  ( ph  ->  B  =  C )
4 3eqtr3d.3 . 2  |-  ( ph  ->  B  =  D )
53, 4eqtr3d 2510 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-cleq 2459
This theorem is referenced by:  mpteqb  5964  fvmptt  5965  fsnunfv  6101  f1ocnvfv1  6170  f1ocnvfv2  6171  fcof1  6178  weniso  6238  caov12d  6480  caov13d  6482  caov411d  6484  caovmo  6496  grprinvlem  6497  grprinvd  6498  grpridd  6499  onovuni  7013  tfrlem5  7049  seqomlem1  7115  seqomlem4  7118  onasuc  7178  onesuc  7180  oeeui  7251  fopwdom  7625  unxpdomlem2  7725  cantnfres  8096  cnfcom2lem  8145  cnfcom2  8146  cnfcom2lemOLD  8153  cnfcom2OLD  8154  cardiun  8363  ackbij1lem16  8615  ackbij2lem2  8620  fpwwe2lem6  9013  fpwwe2lem8  9015  canthp1lem2  9031  mul12  9745  mul4  9748  addid1  9759  addcan  9763  addcom  9765  addcomd  9781  add12  9792  ppncan  9861  addsub4  9862  muladd  9989  mulcand  10182  receu  10194  div13  10228  divdivdiv  10245  divcan5  10246  divdiv1  10255  divdiv2  10256  halfaddsub  10772  uzindOLD  10955  xadddi  11487  xov1plusxeqvd  11666  fztp  11736  flzadd  11927  fldiv  11955  addmodid  12004  modnegd  12010  modsub12d  12012  2submod  12016  seqm1  12092  seqcaopr  12112  seqf1o  12116  expsub  12181  zesq  12257  digit1  12268  discr1  12270  discr  12271  facnn2  12330  faclbnd6  12345  hashfz1  12387  hashdom  12415  hashun  12418  hashbclem  12467  hashfac  12473  seqcoll  12478  wrdlenccats1lenm1  12590  ccatopth  12658  repsw2  12851  repsw3  12852  shftval3  12872  crre  12910  resub  12923  imsub  12931  cjsub  12945  abslem2  13135  sqreulem  13155  climshft2  13368  isercolllem2  13451  iseraltlem2  13468  iseraltlem3  13469  fsumsub  13566  telfsumo  13579  telfsumo2  13580  hashiun  13599  bcxmas  13610  climcndslem1  13624  climcndslem2  13625  trireciplem  13636  geoser  13641  geo2sum2  13646  sinsub  13764  cossub  13765  rpnnen2lem10  13818  ruclem12  13835  divalglem9  13918  bitsinv1lem  13950  bitsinv1  13951  bitsf1  13955  sadasslem  13979  bitsres  13982  smup1  13998  smumul  14002  modgcd  14033  absmulgcd  14044  gcdmultiplez  14048  eucalg  14075  numdensq  14146  dfphi2  14163  phiprm  14166  fermltl  14173  prmdiveq  14175  odzdvds  14181  powm2modprm  14187  modprm0  14189  coprimeprodsq  14192  pythagtriplem6  14204  pythagtriplem7  14205  pythagtriplem12  14209  pythagtriplem16  14213  pcaddlem  14266  sumhash  14274  pcfac  14277  pockthlem  14282  prmreclem6  14298  4sqlem12  14333  4sqlem15  14336  vdwlem3  14360  vdwlem6  14363  vdwlem9  14366  ramub1lem2  14404  cshwshashlem2  14439  divsaddvallem  14806  xpsaddlem  14830  xpsvsca  14834  mrcun  14877  homfeqval  14953  comfeqval  14964  sectcan  15011  sectco  15012  sectmon  15033  monsect  15034  funcsect  15099  setcmon  15272  resscatc  15290  catciso  15292  evlfcllem  15348  curf2cl  15358  curfcl  15359  yonedalem4c  15404  yonedalem3b  15406  yonedainv  15408  latj12  15583  mnd12g  15742  resmhm  15809  pwsco2mhm  15821  frmdup3  15866  grprcan  15893  grplcan  15912  grpinv11  15917  grpinvnz  15919  grplmulf1o  15922  grpinvpropd  15923  grpinvadd  15926  grpsubsub4  15941  mulgz  15973  mulgdirlem  15976  mulgdir  15977  mulgass  15982  mulgsubdir  15983  mulgpropd  15985  pwsmulg  15994  imasgrp2  15995  isnsg3  16040  nmzsubg  16047  ssnmz  16048  eqger  16056  eqglact  16057  ghminv  16079  conjnmz  16105  subgga  16143  gasubg  16145  galcan  16147  gacan  16148  cntzsubg  16179  cntzmhm  16181  psgnunilem2  16326  sylow1lem1  16424  sylow2blem2  16447  sylow2blem3  16448  lsmmod  16499  lsmpropd  16501  lsmdisj2  16506  subgdisj1  16515  subgdisj2  16516  efgredleme  16567  efgredlemd  16568  efgredlemc  16569  efgredlem  16571  frgpup3lem  16601  mulgdi  16641  lsm4  16669  cygabl  16696  gsummhm2  16764  gsummhm2OLD  16765  gsumpt  16791  gsumptOLD  16792  gsum2d  16802  gsum2dOLD  16803  dprdfeq0  16864  dprdfeq0OLD  16871  ablfac1eu  16926  rngcom  17028  isrngd  17034  rnglz  17036  rngrz  17037  rng1eq0  17039  rngmneg1  17043  gsumdixpOLD  17058  gsumdixp  17059  unitgrp  17117  irredrmul  17157  drngmul0or  17217  subrginv  17245  subrgunit  17247  srngnvl  17305  srngadd  17306  srngmul  17307  issrngd  17310  lmodvs0  17346  lmodvneg1  17353  lmodcom  17356  lmodsubdi  17367  lmodvsinv  17482  lmodvsinv2  17483  lmhmvsca  17491  lvecvs0or  17554  lvecinv  17559  lspsnvs  17560  lspabs2  17566  lspfixed  17574  lspsolv  17589  unitrrg  17741  asclpropd  17794  psrass1lem  17828  psrlidm  17855  psrlidmOLD  17856  psrridm  17857  psrridmOLD  17858  mvrf1  17880  mplmon2mul  17965  evlslem1  17983  evlseu  17984  evlssca  17990  evlsvar  17991  coe1pwmul  18119  pf1ind  18190  prmirredlem  18318  prmirredlemOLD  18321  mulgrhm2  18328  mulgrhm2OLD  18331  chrrhm  18363  znidomb  18395  psgnghm  18411  psgninv  18413  zrhpsgnodpm  18423  evpmodpmf1o  18427  psgndiflemB  18431  ip0r  18467  ipdir  18469  ipdi  18470  ipass  18475  ipassr  18476  phlpropd  18485  ocvpj  18543  uvcresum  18619  lmimlbs  18666  gsumcom3  18696  mat0dimbas0  18763  mdetrlin  18899  mdetrsca  18900  mdetr0  18902  mdetunilem8  18916  mdetuni0  18918  mdetmul  18920  maducoeval2  18937  madurid  18941  madulid  18942  matinv  18974  matunit  18975  slesolinv  18977  slesolinvbi  18978  cpmadugsumlemF  19172  restin  19461  cncmp  19686  cmpsublem  19693  conndisj  19711  cnconn  19717  kgencmp2  19810  ufldom  20226  tgplacthmeo  20365  ghmcnp  20376  divstgpopn  20381  divstgphaus  20384  tsmsxplem2  20419  tususp  20538  xpsdsval  20647  blpnfctr  20702  xmssym  20731  ressxms  20791  isngp2  20880  ngppropd  20914  nminvr  20941  blcvx  21066  icccvx  21213  pcohtpylem  21282  pcohtpy  21283  cvsmuleqdivd  21374  cvsdiveqd  21375  pjthlem1  21615  ovollb2lem  21662  ovolicc2lem1  21691  ovolicc2lem5  21695  volsup  21729  ovolioo  21741  uniiccdif  21750  uniioombllem3  21757  uniioombllem4  21758  vitalilem3  21782  itg1sub  21879  itg2const  21910  iblcnlem1  21957  itgcnlem  21959  itgaddlem2  21993  itgsub  21995  itgabs  22004  ditgsplit  22028  dvmulbr  22105  dvcmul  22110  dvcmulf  22111  dvrec  22121  dvmptres3  22122  dvmptadd  22126  dvmptmul  22127  dvmptres2  22128  dvmptneg  22132  dvmptsub  22133  dvmptcj  22134  dvmptco  22138  dveflem  22143  dvlip  22157  dvlipcn  22158  dvlip2  22159  dvcvx  22184  dvfsumle  22185  dvfsumabs  22187  dvfsumlem1  22190  dvfsumlem2  22191  ftc2  22208  ftc2ditglem  22209  itgparts  22211  itgsubstlem  22212  itgsubst  22213  fta1glem1  22329  fta1blem  22332  plyeq0lem  22370  plymullem1  22374  coeeulem  22384  coe0  22415  coesub  22416  dvply1  22442  plydivlem4  22454  plyrem  22463  fta1lem  22465  vieta1  22470  plyexmo  22471  elqaalem2  22478  aareccl  22484  aannenlem1  22486  aaliou3lem2  22501  dvtaylp  22527  taylthlem1  22530  radcnvlem1  22570  pserdvlem2  22585  efcvx  22606  ptolemy  22650  tangtx  22659  efif1olem3  22692  efif1olem4  22693  lognegb  22730  efiarg  22748  cosargd  22749  tanarg  22760  logtayl  22797  cxpsub  22819  cxproot  22827  cxpsqrt  22840  cxpcn3lem  22877  cxpaddlelem  22881  abscxpbnd  22883  root1eq1  22885  cxpeq  22887  logrec  22907  isosctrlem2  22909  isosctrlem3  22910  isosctr  22911  ssscongptld  22912  chordthmlem  22919  heron  22925  quad2  22926  dcubic1lem  22930  mcubic  22934  cubic2  22935  cubic  22936  dquartlem2  22939  dquart  22940  quart1lem  22942  quart1  22943  asinlem2  22956  asinlem3  22958  asinsin  22979  sinacos  22992  atanlogsublem  23002  efiatan2  23004  2efiatan  23005  tanatan  23006  atantan  23010  atans2  23018  dvatan  23022  atantayl  23024  atantayl2  23025  log2cnv  23031  rlimcnp2  23052  cxplim  23057  cxp2lim  23062  cvxcl  23070  scvxcvx  23071  wilthlem1  23098  wilthlem2  23099  ftalem5  23106  basellem3  23112  basellem5  23114  basellem8  23117  mumullem2  23210  musum  23223  musumsum  23224  muinv  23225  sgmppw  23228  1sgmprm  23230  1sgm2ppw  23231  ppiub  23235  logfac2  23248  chpchtsum  23250  perfectlem1  23260  perfectlem2  23261  dchrn0  23281  dchrfi  23286  dchrabs  23291  dchrptlem1  23295  dchrhash  23302  dchr2sum  23304  sum2dchr  23305  bposlem6  23320  bposlem9  23323  lgsvalmod  23346  lgsdilem  23353  lgsne0  23364  lgssq  23366  lgssq2  23367  lgsqr  23377  lgsdchrval  23378  lgsdchr  23379  lgseisenlem1  23380  lgseisenlem2  23381  lgseisenlem4  23383  lgsquadlem1  23385  lgsquadlem3  23387  lgsquad3  23392  m1lgs  23393  rplogsumlem1  23425  rplogsumlem2  23426  dchrisumlem2  23431  dchrisum0fno1  23452  rpvmasum2  23453  dchrisum0lem1  23457  dchrisum0lem2  23459  mudivsum  23471  mulog2sumlem1  23475  vmalogdivsum  23480  2vmadivsumlem  23481  logsqvma  23483  selberglem2  23487  selberg2lem  23491  selberg3lem1  23498  selberg4lem1  23501  selberg4  23502  pntrsumo1  23506  selbergr  23509  selberg34r  23512  pntrlog2bndlem3  23520  pntrlog2bndlem4  23521  pntibndlem2  23532  pntlemg  23539  pntlemr  23543  pntlemf  23546  ostthlem1  23568  padicabvcxp  23573  ostth3  23579  tgcgrcomlr  23627  tgbtwnconn1lem2  23715  tgbtwnconn1lem3  23716  krippenlem  23803  ragcgr  23820  f1otrg  23878  ttgcontlem1  23892  brbtwn2  23912  axsegconlem10  23933  ax5seglem3  23938  ax5seglem6  23941  axpaschlem  23947  axeuclidlem  23969  axcontlem2  23972  axcontlem7  23977  axcontlem8  23978  cusgrasizeindslem3  24179  frgrancvvdeq  24747  frgrancvvdgeq  24748  numclwwlk7  24819  grpoidinvlem1  24910  grpoideu  24915  grporcan  24927  grpolcan  24939  grpoasscan1  24943  grpoinvop  24947  grpopnpcan2  24959  gxsuc  24978  gxsub  24982  gxmul  24984  ablo4  24993  subgoinv  25014  ablomul  25061  ghgrp  25074  ghablo  25075  rngolz  25107  rngorz  25108  zerdivemp1  25140  nvadd12  25220  nvscom  25228  nvmul0or  25251  nvz0  25275  smcnlem  25311  ipidsq  25327  sspz  25352  lno0  25375  lnoadd  25377  lnomul  25379  ipasslem3  25452  dipdi  25462  dipassr  25465  dipsubdi  25468  ubthlem2  25491  hvmul0or  25646  hvadd12  25656  hvadd4  25657  hvmulcom  25664  normneg  25765  pjhthlem1  26013  chj12  26156  spanunsni  26201  5oalem2  26277  3oalem2  26285  mayete3iOLD  26351  hoadd4  26407  homul12  26428  hosubdi  26431  honegsubdi  26433  hosub4  26436  adj2  26557  lnopmul  26590  lnopaddi  26594  lnfnaddi  26666  lnfnmuli  26667  cnlnadjlem6  26695  adjeq0  26714  leopmul  26757  opsqrlem1  26763  opsqrlem6  26768  hstnmoc  26846  strlem1  26873  chirredlem3  27015  fpwrelmapffslem  27255  xaddeq0  27269  bcm1n  27296  divnumden2  27304  xmulcand  27313  xreceu  27314  xrsmulgzz  27356  xrge0adddir  27372  xrge0adddi  27373  abliso  27376  ogrpaddltrbid  27401  ogrpinvlt  27404  archiabllem1a  27425  archiabllem1  27427  archiabllem2c  27429  slmdvs0  27458  dvrcan5  27474  ornglmullt  27488  orngrmullt  27489  rhmunitinv  27503  qqhval2lem  27626  qtophaus  27665  esummulc1  27755  measxun2  27849  measssd  27854  oddpwdc  27961  eulerpartlemgs2  27987  eulerpartlemn  27988  totprobd  28033  signstfvn  28194  signstfveq0  28202  zetacvg  28225  lgamgulmlem4  28242  lgamcvg2  28265  gamp1  28268  subfaclim  28300  cvxscon  28356  rescon  28359  cvmliftmolem1  28394  cvmliftlem7  28404  cvmliftlem13  28409  cvmlift2lem7  28422  cvmlift3lem5  28436  ghomf1olem  28537  fprodm1  28701  fallfacfwd  28763  binomfallfaclem2  28767  faclim2  28778  funsseq  28804  bpolydiflem  29421  bpoly4  29426  fsumcube  29427  ptrest  29653  itg2addnclem  29671  itg2addnclem3  29673  itgaddnclem2  29679  itgsubnc  29682  iblmulc2nc  29685  itgabsnc  29689  ftc2nc  29704  areacirclem1  29712  areacirclem4  29715  areacirc  29717  clsun  29751  topjoin  29814  cocanfo  29839  ablo4pnp  29973  zerdivemp1x  29989  crngm4  30031  crngohomfo  30034  diophrw  30324  eldioph2lem1  30325  pellexlem2  30398  pellexlem6  30402  pellex  30403  pell1234qrne0  30421  pell1234qrreccl  30422  pell1qrgaplem  30441  rmxm1  30502  oddcomabszz  30512  jm2.19lem1  30563  jm3.1lem2  30592  dnnumch3  30625  pwssplit4  30667  flcidc  30756  hashgcdlem  30790  deg1mhm  30800  itgpowd  30815  lcmgcd  30841  lcmid  30843  nzprmdif  30852  hashnzfz  30853  dvsconst  30863  dvsid  30864  expgrowth  30868  itgsinexplem1  31299  itgsinexp  31300  stoweidlem1  31329  wallispi2lem2  31400  stirlinglem3  31404  stirlinglem5  31406  stirlinglem10  31411  stirlinglem15  31416  sigaradd  31578  cevathlem1  31579  imarnf1pr  31804  usgrauvtxvd  31853  bnj1379  32986  bnj1321  33180  bj-bary1lem  33769  fsumshftdOLD  33773  lfl0  33880  lfladd  33881  lflmul  33883  eqlkr3  33916  olm11  34042  latm12  34045  cmtcomlemN  34063  omlspjN  34076  hlatj12  34185  1cvrjat  34289  dalemrotyz  34472  padd12N  34653  pmapjlln1  34669  atmod2i1  34675  pmapocjN  34744  pnonsingN  34747  pexmidN  34783  lhp2at0  34846  lhpelim  34851  ltrncnv  34960  ltrnmw  34965  cdleme7c  35059  cdleme15b  35089  cdlemednpq  35113  cdleme20y  35116  cdleme20m  35137  cdleme22cN  35156  cdleme22d  35157  cdleme23b  35164  cdleme30a  35192  cdleme35h  35270  cdlemeg46frv  35339  cdlemg2fv2  35414  cdlemg2l  35417  cdlemg2m  35418  cdlemg8c  35443  cdlemg10bALTN  35450  cdlemg12  35464  cdlemg13a  35465  cdlemg18c  35494  cdlemg19  35498  trlcoat  35537  cdlemg47  35550  tendo1ne0  35642  cdlemk9  35653  cdlemk9bN  35654  dia2dimlem1  35879  tendolinv  35920  tendorinv  35921  dvhlveclem  35923  doca3N  35942  dihmeetlem7N  36125  dihjatc1  36126  dihmeetlem18N  36139  dochnoncon  36206  dihjatc  36232  dihjatcclem1  36233  dihjatcclem4  36236  dochsnkr  36287  lcfl7lem  36314  lcfl8  36317  lcfl9a  36320  lclkrlem1  36321  lclkrlem2e  36326  lclkrlem2j  36331  lcfrlem1  36357  lcfrlem9  36365  lcfrlem23  36380  lcfrlem31  36388  mapd0  36480  mapdpglem21  36507  baerlem3lem1  36522  baerlem5alem1  36523  mapdindp4  36538  mapdh6gN  36557  hdmap1l6g  36632  hgmapval0  36710  hgmaprnlem1N  36714  hlhilhillem  36778
  Copyright terms: Public domain W3C validator