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

Theorem 3eqtr3d 2478
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 2472 . 2  |-  ( ph  ->  B  =  C )
4 3eqtr3d.3 . 2  |-  ( ph  ->  B  =  D )
53, 4eqtr3d 2472 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-ex 1587  df-cleq 2431
This theorem is referenced by:  mpteqb  5783  fvmptt  5784  fsnunfv  5913  f1ocnvfv1  5978  f1ocnvfv2  5979  fcof1  5986  weniso  6040  caov12d  6279  caov13d  6281  caov411d  6283  caovmo  6295  grprinvlem  6296  grprinvd  6297  grpridd  6298  onovuni  6795  tfrlem5  6831  seqomlem1  6897  seqomlem4  6900  onasuc  6960  onesuc  6962  oeeui  7033  fopwdom  7411  unxpdomlem2  7510  cantnfres  7877  cnfcom2lem  7926  cnfcom2  7927  cnfcom2lemOLD  7934  cnfcom2OLD  7935  cardiun  8144  ackbij1lem16  8396  ackbij2lem2  8401  fpwwe2lem6  8794  fpwwe2lem8  8796  canthp1lem2  8812  mul12  9527  mul4  9530  addid1  9541  addcan  9545  addcom  9547  addcomd  9563  add12  9574  ppncan  9643  addsub4  9644  muladd  9769  mulcand  9961  receu  9973  div13  10007  divdivdiv  10024  divcan5  10025  divdiv1  10034  divdiv2  10035  halfaddsub  10550  uzindOLD  10728  xadddi  11250  xov1plusxeqvd  11423  fztp  11504  flzadd  11663  fldiv  11691  addmodid  11740  modnegd  11746  modsub12d  11748  2submod  11752  seqm1  11815  seqcaopr  11835  seqf1o  11839  expsub  11903  zesq  11979  digit1  11990  discr1  11992  discr  11993  facnn2  12052  faclbnd6  12067  hashfz1  12109  hashdom  12134  hashun  12137  hashbclem  12197  hashfac  12203  seqcoll  12208  wrdlenccats1lenm1  12297  ccatopth  12356  repsw2  12542  repsw3  12543  shftval3  12557  crre  12595  resub  12608  imsub  12616  cjsub  12630  abslem2  12819  sqreulem  12839  climshft2  13052  isercolllem2  13135  iseraltlem2  13152  iseraltlem3  13153  fsumsub  13247  fsumtscopo  13257  fsumtscopo2  13258  hashiun  13277  bcxmas  13290  climcndslem1  13304  climcndslem2  13305  trireciplem  13316  geoser  13321  geo2sum2  13326  sinsub  13444  cossub  13445  rpnnen2lem10  13498  ruclem12  13515  divalglem9  13597  bitsinv1lem  13629  bitsinv1  13630  bitsf1  13634  sadasslem  13658  bitsres  13661  smup1  13677  smumul  13681  modgcd  13712  absmulgcd  13723  gcdmultiplez  13727  eucalg  13754  numdensq  13824  dfphi2  13841  phiprm  13844  fermltl  13851  prmdiveq  13853  odzdvds  13859  modprm0  13865  coprimeprodsq  13868  pythagtriplem6  13880  pythagtriplem7  13881  pythagtriplem12  13885  pythagtriplem16  13889  pcaddlem  13942  sumhash  13950  pcfac  13953  pockthlem  13958  prmreclem6  13974  4sqlem12  14009  4sqlem15  14012  vdwlem3  14036  vdwlem6  14039  vdwlem9  14042  ramub1lem2  14080  cshwshashlem2  14115  divsaddvallem  14481  xpsaddlem  14505  xpsvsca  14509  mrcun  14552  homfeqval  14628  comfeqval  14639  sectcan  14686  sectco  14687  sectmon  14708  monsect  14709  funcsect  14774  setcmon  14947  resscatc  14965  catciso  14967  evlfcllem  15023  curf2cl  15033  curfcl  15034  yonedalem4c  15079  yonedalem3b  15081  yonedainv  15083  latj12  15258  mnd12g  15417  resmhm  15478  pwsco2mhm  15490  frmdup3  15535  grprcan  15562  grplcan  15581  grpinv11  15586  grpinvnz  15588  grplmulf1o  15591  grpinvpropd  15592  grpinvadd  15595  grpsubsub4  15609  mulgz  15639  mulgdirlem  15642  mulgdir  15643  mulgass  15648  mulgsubdir  15649  mulgpropd  15651  pwsmulg  15660  imasgrp2  15661  isnsg3  15706  nmzsubg  15713  ssnmz  15714  eqger  15722  eqglact  15723  ghminv  15745  conjnmz  15771  subgga  15809  gasubg  15811  galcan  15813  gacan  15814  cntzsubg  15845  cntzmhm  15847  psgnunilem2  15992  sylow1lem1  16088  sylow2blem2  16111  sylow2blem3  16112  lsmmod  16163  lsmpropd  16165  lsmdisj2  16170  subgdisj1  16179  subgdisj2  16180  efgredleme  16231  efgredlemd  16232  efgredlemc  16233  efgredlem  16235  frgpup3lem  16265  mulgdi  16305  lsm4  16333  cygabl  16358  gsummhm2  16424  gsummhm2OLD  16425  gsumpt  16444  gsumptOLD  16445  gsum2d  16453  gsum2dOLD  16454  dprdfeq0  16502  dprdfeq0OLD  16509  ablfac1eu  16564  rngcom  16663  isrngd  16669  rnglz  16671  rngrz  16672  rng1eq0  16674  rngmneg1  16677  gsumdixpOLD  16690  gsumdixp  16691  unitgrp  16749  irredrmul  16789  drngmul0or  16833  subrginv  16861  subrgunit  16863  srngnvl  16921  srngadd  16922  srngmul  16923  issrngd  16926  lmodvs0  16962  lmodvneg1  16968  lmodcom  16971  lmodsubdi  16982  lmodvsinv  17097  lmodvsinv2  17098  lmhmvsca  17106  lvecvs0or  17169  lvecinv  17174  lspsnvs  17175  lspabs2  17181  lspfixed  17189  lspsolv  17204  unitrrg  17345  asclpropd  17396  psrass1lem  17427  psrlidm  17454  psrlidmOLD  17455  psrridm  17456  psrridmOLD  17457  mvrf1  17478  mplmon2mul  17563  evlslem1  17581  evlseu  17582  evlssca  17588  evlsvar  17589  coe1pwmul  17712  pf1ind  17769  prmirredlem  17897  prmirredlemOLD  17900  mulgrhm2  17907  mulgrhm2OLD  17910  chrrhm  17942  znidomb  17974  psgnghm  17990  psgninv  17992  zrhpsgnodpm  18002  evpmodpmf1o  18006  psgndiflemB  18010  ip0r  18046  ipdir  18048  ipdi  18049  ipass  18054  ipassr  18055  phlpropd  18064  ocvpj  18122  uvcresum  18198  lmimlbs  18245  gsumcom3  18279  mat0dimbas0  18305  mdetrlin  18389  mdetrsca  18390  mdetr0  18392  mdetunilem8  18405  mdetuni0  18407  mdetmul  18409  maducoeval2  18426  madurid  18430  madulid  18431  matinv  18463  matunit  18464  slesolinv  18466  slesolinvbi  18467  restin  18750  cncmp  18975  cmpsublem  18982  conndisj  19000  cnconn  19006  kgencmp2  19099  ufldom  19515  tgplacthmeo  19654  ghmcnp  19665  divstgpopn  19670  divstgphaus  19673  tsmsxplem2  19708  tususp  19827  xpsdsval  19936  blpnfctr  19991  xmssym  20020  ressxms  20080  isngp2  20169  ngppropd  20203  nminvr  20230  blcvx  20355  icccvx  20502  pcohtpylem  20571  pcohtpy  20572  cvsmuleqdivd  20663  cvsdiveqd  20664  pjthlem1  20904  ovollb2lem  20951  ovolicc2lem1  20980  ovolicc2lem5  20984  volsup  21017  ovolioo  21029  uniiccdif  21038  uniioombllem3  21045  uniioombllem4  21046  vitalilem3  21070  itg1sub  21167  itg2const  21198  iblcnlem1  21245  itgcnlem  21247  itgaddlem2  21281  itgsub  21283  itgabs  21292  ditgsplit  21316  dvmulbr  21393  dvcmul  21398  dvcmulf  21399  dvrec  21409  dvmptres3  21410  dvmptadd  21414  dvmptmul  21415  dvmptres2  21416  dvmptneg  21420  dvmptsub  21421  dvmptcj  21422  dvmptco  21426  dveflem  21431  dvlip  21445  dvlipcn  21446  dvlip2  21447  dvcvx  21472  dvfsumle  21473  dvfsumabs  21475  dvfsumlem1  21478  dvfsumlem2  21479  ftc2  21496  ftc2ditglem  21497  itgparts  21499  itgsubstlem  21500  itgsubst  21501  fta1glem1  21617  fta1blem  21620  plyeq0lem  21658  plymullem1  21662  coeeulem  21672  coe0  21703  coesub  21704  dvply1  21730  plydivlem4  21742  plyrem  21751  fta1lem  21753  vieta1  21758  plyexmo  21759  elqaalem2  21766  aareccl  21772  aannenlem1  21774  aaliou3lem2  21789  dvtaylp  21815  taylthlem1  21818  radcnvlem1  21858  pserdvlem2  21873  efcvx  21894  ptolemy  21938  tangtx  21947  efif1olem3  21980  efif1olem4  21981  lognegb  22018  efiarg  22036  cosargd  22037  tanarg  22048  logtayl  22085  cxpsub  22107  cxproot  22115  cxpsqr  22128  cxpcn3lem  22165  cxpaddlelem  22169  abscxpbnd  22171  root1eq1  22173  cxpeq  22175  logrec  22195  isosctrlem2  22197  isosctrlem3  22198  isosctr  22199  ssscongptld  22200  chordthmlem  22207  heron  22213  quad2  22214  dcubic1lem  22218  mcubic  22222  cubic2  22223  cubic  22224  dquartlem2  22227  dquart  22228  quart1lem  22230  quart1  22231  asinlem2  22244  asinlem3  22246  asinsin  22267  sinacos  22280  atanlogsublem  22290  efiatan2  22292  2efiatan  22293  tanatan  22294  atantan  22298  atans2  22306  dvatan  22310  atantayl  22312  atantayl2  22313  log2cnv  22319  rlimcnp2  22340  cxplim  22345  cxp2lim  22350  cvxcl  22358  scvxcvx  22359  wilthlem1  22386  wilthlem2  22387  ftalem5  22394  basellem3  22400  basellem5  22402  basellem8  22405  mumullem2  22498  musum  22511  musumsum  22512  muinv  22513  sgmppw  22516  1sgmprm  22518  1sgm2ppw  22519  ppiub  22523  logfac2  22536  chpchtsum  22538  perfectlem1  22548  perfectlem2  22549  dchrn0  22569  dchrfi  22574  dchrabs  22579  dchrptlem1  22583  dchrhash  22590  dchr2sum  22592  sum2dchr  22593  bposlem6  22608  bposlem9  22611  lgsvalmod  22634  lgsdilem  22641  lgsne0  22652  lgssq  22654  lgssq2  22655  lgsqr  22665  lgsdchrval  22666  lgsdchr  22667  lgseisenlem1  22668  lgseisenlem2  22669  lgseisenlem4  22671  lgsquadlem1  22673  lgsquadlem3  22675  lgsquad3  22680  m1lgs  22681  rplogsumlem1  22713  rplogsumlem2  22714  dchrisumlem2  22719  dchrisum0fno1  22740  rpvmasum2  22741  dchrisum0lem1  22745  dchrisum0lem2  22747  mudivsum  22759  mulog2sumlem1  22763  vmalogdivsum  22768  2vmadivsumlem  22769  logsqvma  22771  selberglem2  22775  selberg2lem  22779  selberg3lem1  22786  selberg4lem1  22789  selberg4  22790  pntrsumo1  22794  selbergr  22797  selberg34r  22800  pntrlog2bndlem3  22808  pntrlog2bndlem4  22809  pntibndlem2  22820  pntlemg  22827  pntlemr  22831  pntlemf  22834  ostthlem1  22856  padicabvcxp  22861  ostth3  22867  tgcgrcomlr  22914  tgbtwnconn1lem2  22985  tgbtwnconn1lem3  22986  krippenlem  23061  ragcgr  23077  f1otrg  23085  ttgcontlem1  23099  brbtwn2  23119  axsegconlem10  23140  ax5seglem3  23145  ax5seglem6  23148  axpaschlem  23154  axeuclidlem  23176  axcontlem2  23179  axcontlem7  23184  axcontlem8  23185  cusgrasizeindslem3  23351  grpoidinvlem1  23659  grpoideu  23664  grporcan  23676  grpolcan  23688  grpoasscan1  23692  grpoinvop  23696  grpopnpcan2  23708  gxsuc  23727  gxsub  23731  gxmul  23733  ablo4  23742  subgoinv  23763  ablomul  23810  ghgrp  23823  ghablo  23824  rngolz  23856  rngorz  23857  zerdivemp1  23889  nvadd12  23969  nvscom  23977  nvmul0or  24000  nvz0  24024  smcnlem  24060  ipidsq  24076  sspz  24101  lno0  24124  lnoadd  24126  lnomul  24128  ipasslem3  24201  dipdi  24211  dipassr  24214  dipsubdi  24217  ubthlem2  24240  hvmul0or  24395  hvadd12  24405  hvadd4  24406  hvmulcom  24413  normneg  24514  pjhthlem1  24762  chj12  24905  spanunsni  24950  5oalem2  25026  3oalem2  25034  mayete3iOLD  25100  hoadd4  25156  homul12  25177  hosubdi  25180  honegsubdi  25182  hosub4  25185  adj2  25306  lnopmul  25339  lnopaddi  25343  lnfnaddi  25415  lnfnmuli  25416  cnlnadjlem6  25444  adjeq0  25463  leopmul  25506  opsqrlem1  25512  opsqrlem6  25517  hstnmoc  25595  strlem1  25622  chirredlem3  25764  fpwrelmapffslem  26000  xaddeq0  26014  bcm1n  26047  divnumden2  26055  xmulcand  26064  xreceu  26065  xrsmulgzz  26107  xrge0adddir  26123  xrge0adddi  26124  abliso  26127  ogrpaddltrbid  26152  ogrpinvlt  26155  archiabllem1a  26176  archiabllem1  26178  archiabllem2c  26180  slmdvs0  26209  dvrcan5  26229  ornglmullt  26243  orngrmullt  26244  rhmunitinv  26258  qqhval2lem  26379  esummulc1  26499  measxun2  26593  measssd  26598  oddpwdc  26706  eulerpartlemgs2  26732  eulerpartlemn  26733  totprobd  26778  signstfvn  26939  signstfveq0  26947  zetacvg  26970  lgamgulmlem4  26987  lgamcvg2  27010  gamp1  27013  subfaclim  27045  cvxscon  27101  rescon  27104  cvmliftmolem1  27139  cvmliftlem7  27149  cvmliftlem13  27154  cvmlift2lem7  27167  cvmlift3lem5  27181  ghomf1olem  27282  fprodm1  27446  fallfacfwd  27508  binomfallfaclem2  27512  faclim2  27523  funsseq  27549  bpolydiflem  28166  bpoly4  28171  fsumcube  28172  ptrest  28396  itg2addnclem  28414  itg2addnclem3  28416  itgaddnclem2  28422  itgsubnc  28425  iblmulc2nc  28428  itgabsnc  28432  ftc2nc  28447  areacirclem1  28455  areacirclem4  28458  areacirc  28460  clsun  28494  topjoin  28557  cocanfo  28582  ablo4pnp  28716  zerdivemp1x  28732  crngm4  28774  crngohomfo  28777  diophrw  29068  eldioph2lem1  29069  pellexlem2  29142  pellexlem6  29146  pellex  29147  pell1234qrne0  29165  pell1234qrreccl  29166  pell1qrgaplem  29185  rmxm1  29246  oddcomabszz  29256  jm2.19lem1  29309  jm3.1lem2  29338  dnnumch3  29371  pwssplit4  29413  flcidc  29502  hashgcdlem  29536  deg1mhm  29546  itgpowd  29561  dvsconst  29575  dvsid  29576  expgrowth  29580  itgsinexplem1  29765  itgsinexp  29766  stoweidlem1  29767  wallispi2lem2  29838  stirlinglem3  29842  stirlinglem5  29844  stirlinglem10  29849  stirlinglem15  29854  sigaradd  29873  cevathlem1  29874  imarnf1pr  30121  powm2modprm  30219  usgrauvtxvd  30501  frgrancvvdeq  30606  frgrancvvdgeq  30607  numclwwlk7  30678  bnj1379  31753  bnj1321  31947  bj-bary1lem  32494  lfl0  32603  lfladd  32604  lflmul  32606  eqlkr3  32639  olm11  32765  latm12  32768  cmtcomlemN  32786  omlspjN  32799  hlatj12  32908  1cvrjat  33012  dalemrotyz  33195  padd12N  33376  pmapjlln1  33392  atmod2i1  33398  pmapocjN  33467  pnonsingN  33470  pexmidN  33506  lhp2at0  33569  lhpelim  33574  ltrncnv  33683  ltrnmw  33688  cdleme7c  33782  cdleme15b  33812  cdlemednpq  33836  cdleme20y  33839  cdleme20m  33860  cdleme22cN  33879  cdleme22d  33880  cdleme23b  33887  cdleme30a  33915  cdleme35h  33993  cdlemeg46frv  34062  cdlemg2fv2  34137  cdlemg2l  34140  cdlemg2m  34141  cdlemg8c  34166  cdlemg10bALTN  34173  cdlemg12  34187  cdlemg13a  34188  cdlemg18c  34217  cdlemg19  34221  trlcoat  34260  cdlemg47  34273  tendo1ne0  34365  cdlemk9  34376  cdlemk9bN  34377  dia2dimlem1  34602  tendolinv  34643  tendorinv  34644  dvhlveclem  34646  doca3N  34665  dihmeetlem7N  34848  dihjatc1  34849  dihmeetlem18N  34862  dochnoncon  34929  dihjatc  34955  dihjatcclem1  34956  dihjatcclem4  34959  dochsnkr  35010  lcfl7lem  35037  lcfl8  35040  lcfl9a  35043  lclkrlem1  35044  lclkrlem2e  35049  lclkrlem2j  35054  lcfrlem1  35080  lcfrlem9  35088  lcfrlem23  35103  lcfrlem31  35111  mapd0  35203  mapdpglem21  35230  baerlem3lem1  35245  baerlem5alem1  35246  mapdindp4  35261  mapdh6gN  35280  hdmap1l6g  35355  hgmapval0  35433  hgmaprnlem1N  35437  hlhilhillem  35501
  Copyright terms: Public domain W3C validator