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 1437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-cleq 2421
This theorem is referenced by:  mpteqb  5980  fvmptt  5981  fsnunfv  6119  f1ocnvfv1  6190  f1ocnvfv2  6191  fcof1  6200  weniso  6260  caov12d  6504  caov13d  6506  caov411d  6508  caovmo  6520  grprinvlem  6521  grprinvd  6522  grpridd  6523  onovuni  7069  tfrlem5  7106  seqomlem1  7175  seqomlem4  7178  onasuc  7238  onesuc  7240  oeeui  7311  fopwdom  7686  unxpdomlem2  7783  cantnfres  8181  cnfcom2lem  8205  cnfcom2  8206  cardiun  8415  ackbij1lem16  8663  ackbij2lem2  8668  fpwwe2lem6  9059  fpwwe2lem8  9061  canthp1lem2  9077  mul12  9798  mul4  9801  addid1  9812  addcan  9816  addcom  9818  addcomd  9834  add12  9845  ppncan  9915  addsub4  9916  muladd  10050  mulcand  10244  receu  10256  div13  10290  divdivdiv  10307  divcan5  10308  divdiv1  10317  divdiv2  10318  halfaddsub  10846  xadddi  11581  xov1plusxeqvd  11776  fztp  11850  flzadd  12056  fldiv  12084  modnegd  12142  modsub12d  12144  2submod  12148  seqm1  12227  seqcaopr  12247  seqf1o  12251  exprec  12310  expsub  12317  zesq  12392  digit1  12403  discr1  12405  discr  12406  facnn2  12465  faclbnd6  12481  hashfz1  12526  hashdom  12555  hashun  12558  hashbclem  12610  hashfac  12616  seqcoll  12621  ccatopth  12811  repsw2  13004  repsw3  13005  shftval3  13118  crre  13156  resub  13169  imsub  13177  cjsub  13191  abslem2  13381  sqreulem  13401  climshft2  13624  isercolllem2  13707  iseraltlem2  13727  iseraltlem3  13728  fsumsub  13827  telfsumo  13840  telfsumo2  13841  hashiun  13860  bcxmas  13871  climcndslem1  13885  climcndslem2  13886  trireciplem  13898  geoser  13903  geo2sum2  13908  fprodm1  13999  fallfacfwd  14067  binomfallfaclem2  14071  bpolydiflem  14085  bpoly4  14090  fsumcube  14091  sinsub  14200  cossub  14201  rpnnen2lem10  14254  ruclem12  14271  divalglem9  14357  bitsinv1lem  14389  bitsinv1  14390  bitsf1  14394  sadasslem  14418  bitsres  14421  smup1  14437  smumul  14441  modgcd  14474  absmulgcd  14486  gcdmultiplez  14490  eucalg  14517  lcmgcd  14537  lcmid  14539  lcmftp  14571  numdensq  14665  dfphi2  14682  phiprm  14685  fermltl  14692  prmdiveq  14694  odzdvds  14700  powm2modprm  14708  modprm0  14710  coprimeprodsq  14713  pythagtriplem6  14725  pythagtriplem7  14726  pythagtriplem12  14730  pythagtriplem16  14734  pcaddlem  14787  sumhash  14795  pcfac  14798  pockthlem  14803  prmreclem6  14819  4sqlem12  14854  4sqlem15OLD  14857  4sqlem15  14863  vdwlem3  14887  vdwlem6  14890  vdwlem9  14893  ramub1lem2  14939  cshwshashlem2  15021  qusaddvallem  15399  xpsaddlem  15423  xpsvsca  15427  mrcun  15470  homfeqval  15544  comfeqval  15555  sectcan  15602  sectco  15603  sectmon  15629  monsect  15630  funcsect  15719  setcmon  15924  resscatc  15942  catciso  15944  evlfcllem  16048  curf2cl  16058  curfcl  16059  yonedalem4c  16104  yonedalem3b  16106  yonedainv  16108  latj12  16284  mnd12g  16494  resmhm  16548  pwsco2mhm  16560  frmdup3lem  16592  grprcan  16641  grplcan  16660  grpinv11  16665  grpinvnz  16667  grplmulf1o  16670  grpinvpropd  16671  grpinvadd  16674  grpsubsub4  16689  mulgz  16721  mulgdirlem  16724  mulgdir  16725  mulgass  16730  mulgsubdir  16731  mulgpropd  16733  pwsmulg  16742  imasgrp2  16743  mhmid  16749  mhmmnd  16750  isnsg3  16793  nmzsubg  16800  ssnmz  16801  eqger  16809  eqglact  16810  ghminv  16832  conjnmz  16858  subgga  16896  gasubg  16898  galcan  16900  gacan  16901  cntzsubg  16932  cntzmhm  16934  psgnunilem2  17078  sylow1lem1  17176  sylow2blem2  17199  sylow2blem3  17200  lsmmod  17251  lsmpropd  17253  lsmdisj2  17258  subgdisj1  17267  subgdisj2  17268  efgredleme  17319  efgredlemd  17320  efgredlemc  17321  efgredlem  17323  frgpup3lem  17353  mulgdi  17393  ghmcmn  17398  lsm4  17424  cygabl  17451  gsummhm2  17498  gsumpt  17520  gsum2d  17530  dprdfeq0  17581  ablfac1eu  17632  ringcom  17735  isringd  17741  ringlz  17743  ringrz  17744  ring1eq0  17746  ringmneg1  17750  gsumdixp  17763  unitgrp  17821  irredrmul  17861  drngmul0or  17922  subrginv  17950  subrgunit  17952  abvrec  17990  srngnvl  18010  srngadd  18011  srngmul  18012  issrngd  18015  lmodvs0  18051  lmodvneg1  18057  lmodcom  18060  lmodsubdi  18071  lmodvsinv  18185  lmodvsinv2  18186  lmhmvsca  18194  lvecvs0or  18257  lvecinv  18262  lspsnvs  18263  lspabs2  18269  lspfixed  18277  lspsolv  18292  unitrrg  18443  asclpropd  18496  psrass1lem  18527  psrlidm  18553  psrridm  18554  mvrf1  18575  mplmon2mul  18650  evlslem1  18664  evlseu  18665  evlssca  18671  evlsvar  18672  coe1pwmul  18798  pf1ind  18869  prmirredlem  18986  mulgrhm2  18992  chrrhm  19024  znidomb  19054  psgnghm  19070  psgninv  19072  zrhpsgnodpm  19082  evpmodpmf1o  19086  psgndiflemB  19090  ip0r  19126  ipdir  19128  ipdi  19129  ipass  19134  ipassr  19135  phlpropd  19144  ocvpj  19202  uvcresum  19273  lmimlbs  19316  gsumcom3  19346  mat0dimbas0  19413  mdetrlin  19549  mdetrsca  19550  mdetr0  19552  mdetunilem8  19566  mdetuni0  19568  mdetmul  19570  maducoeval2  19587  madurid  19591  madulid  19592  matinv  19624  matunit  19625  slesolinv  19627  slesolinvbi  19628  cpmadugsumlemF  19822  restin  20104  cncmp  20329  cmpsublem  20336  conndisj  20353  cnconn  20359  kgencmp2  20483  ufldom  20899  tgplacthmeo  21040  ghmcnp  21051  qustgpopn  21056  qustgphaus  21059  tsmsxplem2  21090  tususp  21209  xpsdsval  21318  blpnfctr  21373  xmssym  21402  ressxms  21462  isngp2  21533  ngppropd  21567  nminvr  21594  blcvx  21718  icccvx  21865  pcohtpylem  21934  pcohtpy  21935  cvsmuleqdivd  22026  cvsdiveqd  22027  pjthlem1  22263  ovollb2lem  22310  ovolicc2lem1  22339  ovolicc2lem5  22343  volsup  22377  ovolioo  22389  uniiccdif  22403  uniioombllem3  22411  uniioombllem4  22412  vitalilem3  22436  itg1sub  22535  itg2const  22566  iblcnlem1  22613  itgcnlem  22615  itgaddlem2  22649  itgsub  22651  itgabs  22660  ditgsplit  22684  dvmulbr  22761  dvcmul  22766  dvcmulf  22767  dvrec  22777  dvmptres3  22778  dvmptadd  22782  dvmptmul  22783  dvmptres2  22784  dvmptneg  22788  dvmptsub  22789  dvmptcj  22790  dvmptco  22794  dveflem  22799  dvlip  22813  dvlipcn  22814  dvlip2  22815  dvcvx  22840  dvfsumle  22841  dvfsumabs  22843  dvfsumlem1  22846  dvfsumlem2  22847  ftc2  22864  ftc2ditglem  22865  itgparts  22867  itgsubstlem  22868  itgsubst  22869  fta1glem1  22982  fta1blem  22985  plyeq0lem  23023  plymullem1  23027  coeeulem  23037  coe0  23069  coesub  23070  dvply1  23096  plydivlem4  23108  plyrem  23117  fta1lem  23119  vieta1  23124  plyexmo  23125  elqaalem2  23132  aareccl  23138  aannenlem1  23140  aaliou3lem2  23155  dvtaylp  23181  taylthlem1  23184  radcnvlem1  23224  pserdvlem2  23239  efcvx  23260  ptolemy  23307  tangtx  23316  efif1olem3  23349  efif1olem4  23350  efabl  23355  lognegb  23395  efiarg  23412  cosargd  23413  tanarg  23424  logtayl  23461  cxpneg  23482  cxpsub  23483  cxprec  23487  cxproot  23491  cxpsqrt  23504  cxpcn3lem  23543  cxpaddlelem  23547  abscxpbnd  23549  root1eq1  23551  cxpeq  23553  logrec  23556  isosctrlem2  23604  isosctrlem3  23605  isosctr  23606  ssscongptld  23607  chordthmlem  23614  heron  23620  quad2  23621  dcubic1lem  23625  mcubic  23629  cubic2  23630  cubic  23631  dquartlem2  23634  dquart  23635  quart1lem  23637  quart1  23638  asinlem2  23651  asinlem3  23653  asinsin  23674  sinacos  23687  atanlogsublem  23697  efiatan2  23699  2efiatan  23700  tanatan  23701  atantan  23705  atans2  23713  dvatan  23717  atantayl  23719  atantayl2  23720  log2cnv  23726  rlimcnp2  23748  cxplim  23753  cxp2lim  23758  cvxcl  23766  scvxcvx  23767  zetacvg  23796  lgamgulmlem4  23813  lgamcvg2  23836  gamp1  23839  wilthlem1  23849  wilthlem2  23850  ftalem5  23857  basellem3  23863  basellem5  23865  basellem8  23868  mumullem2  23961  musum  23974  musumsum  23975  muinv  23976  sgmppw  23979  1sgmprm  23981  1sgm2ppw  23982  ppiub  23986  logfac2  23999  chpchtsum  24001  perfectlem1  24011  perfectlem2  24012  dchrn0  24032  dchrfi  24037  dchrabs  24042  dchrptlem1  24046  dchrhash  24053  dchr2sum  24055  sum2dchr  24056  bposlem6  24071  bposlem9  24074  lgsvalmod  24097  lgsdilem  24104  lgsne0  24115  lgssq  24117  lgssq2  24118  lgsqr  24128  lgsdchrval  24129  lgsdchr  24130  lgseisenlem1  24131  lgseisenlem2  24132  lgseisenlem4  24134  lgsquadlem1  24136  lgsquadlem3  24138  lgsquad3  24143  m1lgs  24144  rplogsumlem1  24176  rplogsumlem2  24177  dchrisumlem2  24182  dchrisum0fno1  24203  rpvmasum2  24204  dchrisum0lem1  24208  dchrisum0lem2  24210  mudivsum  24222  mulog2sumlem1  24226  vmalogdivsum  24231  2vmadivsumlem  24232  logsqvma  24234  selberglem2  24238  selberg2lem  24242  selberg3lem1  24249  selberg4lem1  24252  selberg4  24253  pntrsumo1  24257  selbergr  24260  selberg34r  24263  pntrlog2bndlem3  24271  pntrlog2bndlem4  24272  pntibndlem2  24283  pntlemg  24290  pntlemr  24294  pntlemf  24297  ostthlem1  24319  padicabvcxp  24324  ostth3  24330  tgcgrcomlr  24378  tgifscgr  24407  tgbtwnconn1lem2  24469  tgbtwnconn1lem3  24470  miduniq2  24580  krippenlem  24583  ragcgr  24600  f1otrg  24738  ttgcontlem1  24752  brbtwn2  24772  axsegconlem10  24793  ax5seglem3  24798  ax5seglem6  24801  axpaschlem  24807  axeuclidlem  24829  axcontlem2  24832  axcontlem7  24837  axcontlem8  24838  cusgrasizeindslem3  25039  frgrancvvdeq  25606  frgrancvvdgeq  25607  numclwwlk7  25678  grpoidinvlem1  25768  grpoideu  25773  grporcan  25785  grpolcan  25797  grpoasscan1  25801  grpoinvop  25805  grpopnpcan2  25817  gxsuc  25836  gxsub  25840  gxmul  25842  ablo4  25851  subgoinv  25872  ablomul  25919  ghgrpOLD  25932  ghabloOLD  25933  rngolz  25965  rngorz  25966  zerdivemp1  25998  nvadd12  26078  nvscom  26086  nvmul0or  26109  nvz0  26133  smcnlem  26169  ipidsq  26185  sspz  26210  lno0  26233  lnoadd  26235  lnomul  26237  ipasslem3  26310  dipdi  26320  dipassr  26323  dipsubdi  26326  ubthlem2  26349  hvmul0or  26504  hvadd12  26514  hvadd4  26515  hvmulcom  26522  normneg  26623  pjhthlem1  26870  chj12  27013  spanunsni  27058  5oalem2  27134  3oalem2  27142  hoadd4  27263  homul12  27284  hosubdi  27287  honegsubdi  27289  hosub4  27292  adj2  27413  lnopmul  27446  lnopaddi  27450  lnfnaddi  27522  lnfnmuli  27523  cnlnadjlem6  27551  adjeq0  27570  leopmul  27613  opsqrlem1  27619  opsqrlem6  27624  hstnmoc  27702  strlem1  27729  chirredlem3  27871  fpwrelmapffslem  28151  subeqxfrd  28155  addeqxfrd  28156  xaddeq0  28164  bcm1n  28198  divnumden2  28210  xmulcand  28219  xreceu  28220  bhmafibid1  28234  2sqmod  28238  xrsmulgzz  28268  xrge0adddir  28284  xrge0adddi  28285  abliso  28288  ogrpaddltrbid  28313  ogrpinvlt  28316  archiabllem1a  28337  archiabllem1  28339  archiabllem2c  28341  slmdvs0  28370  dvrcan5  28386  ornglmullt  28400  orngrmullt  28401  rhmunitinv  28415  mdetpmtr2  28480  madjusmdetlem1  28483  mdetlap  28488  qtophaus  28493  qqhval2lem  28615  esumpad  28706  esummulc1  28732  esumsup  28740  measxun2  28862  measssd  28867  inelcarsg  28963  carsggect  28970  carsgclctunlem2  28971  pmeasmono  28976  oddpwdc  29004  eulerpartlemgs2  29030  eulerpartlemn  29031  totprobd  29076  signstfvn  29237  signstfveq0  29245  bnj1379  29421  bnj1321  29615  subfaclim  29690  cvxscon  29745  rescon  29748  cvmliftmolem1  29783  cvmliftlem7  29793  cvmliftlem13  29798  cvmlift2lem7  29811  cvmlift3lem5  29825  elmsta  29965  msubff1  29973  mthmpps  29999  ghomf1olem  30091  bcm1nt  30151  faclim2  30162  funsseq  30187  clsun  30760  topjoin  30797  bj-bary1lem  31451  ptrest  31633  poimirlem4  31638  poimirlem6  31640  poimirlem7  31641  poimirlem9  31643  poimirlem11  31645  poimirlem12  31646  poimirlem26  31660  poimirlem27  31661  itg2addnclem  31687  itg2addnclem3  31689  itgaddnclem2  31695  itgsubnc  31698  iblmulc2nc  31701  itgabsnc  31705  ftc2nc  31720  areacirclem1  31726  areacirclem4  31729  areacirc  31731  cocanfo  31738  ablo4pnp  31872  zerdivemp1x  31888  crngm4  31930  crngohomfo  31933  fsumshftdOLD  32223  lfl0  32330  lfladd  32331  lflmul  32333  eqlkr3  32366  olm11  32492  latm12  32495  cmtcomlemN  32513  omlspjN  32526  hlatj12  32635  1cvrjat  32739  dalemrotyz  32922  padd12N  33103  pmapjlln1  33119  atmod2i1  33125  pmapocjN  33194  pnonsingN  33197  pexmidN  33233  lhp2at0  33296  lhpelim  33301  ltrncnv  33410  ltrnmwOLD  33416  cdleme7c  33510  cdleme15b  33540  cdlemednpq  33564  cdleme20yOLD  33568  cdleme20m  33589  cdleme22cN  33608  cdleme22d  33609  cdleme23b  33616  cdleme30a  33644  cdleme35h  33722  cdlemeg46frv  33791  cdlemg2fv2  33866  cdlemg2l  33869  cdlemg2m  33870  cdlemg8c  33895  cdlemg10bALTN  33902  cdlemg12  33916  cdlemg13a  33917  cdlemg18c  33946  cdlemg19  33950  trlcoat  33989  cdlemg47  34002  tendo1ne0  34094  cdlemk9  34105  cdlemk9bN  34106  dia2dimlem1  34331  tendolinv  34372  tendorinv  34373  dvhlveclem  34375  doca3N  34394  dihmeetlem7N  34577  dihjatc1  34578  dihmeetlem18N  34591  dochnoncon  34658  dihjatc  34684  dihjatcclem1  34685  dihjatcclem4  34688  dochsnkr  34739  lcfl7lem  34766  lcfl8  34769  lcfl9a  34772  lclkrlem1  34773  lclkrlem2e  34778  lclkrlem2j  34783  lcfrlem1  34809  lcfrlem9  34817  lcfrlem23  34832  lcfrlem31  34840  mapd0  34932  mapdpglem21  34959  baerlem3lem1  34974  baerlem5alem1  34975  mapdindp4  34990  mapdh6gN  35009  hdmap1l6g  35084  hgmapval0  35162  hgmaprnlem1N  35166  hlhilhillem  35230  diophrw  35300  eldioph2lem1  35301  pellexlem2  35374  pellexlem6  35378  pellex  35379  pell1234qrne0  35397  pell1234qrreccl  35398  pell1qrgaplem  35417  rmxm1  35478  oddcomabszz  35488  jm2.19lem1  35540  jm3.1lem2  35569  dnnumch3  35601  pwssplit4  35643  flcidc  35729  hashgcdlem  35763  deg1mhm  35773  itgpowd  35788  radcnvrat  36290  nzprmdif  36295  hashnzfz  36296  dvsconst  36306  dvsid  36307  expgrowth  36311  bccm1k  36318  bccn1  36320  binomcxplemnotnn0  36332  subadd4b  37091  sumnnodd  37272  icccncfext  37327  dvresntr  37350  itgsinexplem1  37389  itgsinexp  37390  stoweidlem1  37420  wallispi2lem2  37493  stirlinglem3  37497  stirlinglem5  37499  stirlinglem10  37504  stirlinglem15  37509  dirkertrigeqlem3  37521  dirkercncflem2  37525  fourierdlem26  37554  fourierdlem42  37570  fourierdlem66  37594  fourierdlem73  37601  fourierdlem81  37609  fourierdlem83  37611  fourierdlem107  37635  etransclem23  37679  sigaradd  37865  cevathlem1  37866  m1mod0mod1  38103  mod2eq1n2dvds  38105  perfectALTVlem1  38223  perfectALTVlem2  38224  proththd  38294  imarnf1pr  38376  usgrauvtxvd  38418  rnglz  38632  pw2m1lepw2m1  39069  nnpw2pmod  39145  dignn0flhalflem1  39177  aacllem  39291
  Copyright terms: Public domain W3C validator