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

Theorem 3eqtr3d 2427
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 2421 . 2  |-  ( ph  ->  B  =  C )
4 3eqtr3d.3 . 2  |-  ( ph  ->  B  =  D )
53, 4eqtr3d 2421 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649
This theorem is referenced by:  mpteqb  5758  fvmptt  5759  fsnunfv  5872  f1ocnvfv1  5953  f1ocnvfv2  5954  fcof1  5959  weniso  6014  caov12d  6207  caov13d  6209  caov411d  6211  caovmo  6223  grprinvlem  6224  grprinvd  6225  grpridd  6226  onovuni  6540  seqomlem1  6643  seqomlem4  6646  onasuc  6708  onesuc  6710  oeeui  6781  fopwdom  7152  unxpdomlem2  7250  cantnfres  7566  cnfcom2lem  7591  cnfcom2  7592  cardiun  7802  ackbij1lem16  8048  ackbij2lem2  8053  fpwwe2lem6  8443  fpwwe2lem8  8445  canthp1lem2  8461  mul12  9164  mul4  9167  addid1  9178  addcan  9182  addcom  9184  addcomd  9200  add12  9211  ppncan  9275  addsub4  9276  muladd  9398  mulcand  9587  receu  9599  div13  9631  divdivdiv  9647  divcan5  9648  divdiv1  9657  divdiv2  9658  halfaddsub  10133  uzindOLD  10296  xadddi  10806  xov1plusxeqvd  10973  fztp  11034  flzadd  11155  fldiv  11168  modnegd  11208  modsub12d  11210  seqm1  11267  seqcaopr  11287  seqf1o  11291  expsub  11354  zesq  11429  digit1  11440  discr1  11442  discr  11443  facnn2  11502  faclbnd6  11517  hashfz1  11557  hashdom  11580  hashun  11583  hashbclem  11628  hashfac  11634  seqcoll  11639  ccatopth  11703  shftval3  11818  crre  11846  resub  11859  imsub  11867  cjsub  11881  abslem2  12070  sqreulem  12090  climshft2  12303  isercolllem2  12386  iseraltlem2  12403  iseraltlem3  12404  fsumsub  12498  fsumtscopo  12508  fsumtscopo2  12509  hashiun  12528  bcxmas  12542  climcndslem1  12556  climcndslem2  12557  trireciplem  12568  geoser  12573  geo2sum2  12578  sinsub  12696  cossub  12697  rpnnen2lem10  12750  ruclem12  12767  divalglem9  12848  bitsinv1lem  12880  bitsinv1  12881  bitsf1  12885  sadasslem  12909  bitsres  12912  smup1  12928  smumul  12932  modgcd  12963  absmulgcd  12974  gcdmultiplez  12978  eucalg  13005  numdensq  13073  dfphi2  13090  phiprm  13093  fermltl  13100  prmdiveq  13102  odzdvds  13108  coprimeprodsq  13110  pythagtriplem6  13122  pythagtriplem7  13123  pythagtriplem12  13127  pythagtriplem16  13131  pcaddlem  13184  sumhash  13192  pcfac  13195  pockthlem  13200  prmreclem6  13216  4sqlem12  13251  4sqlem15  13254  vdwlem3  13278  vdwlem6  13281  vdwlem9  13284  ramub1lem2  13322  divsaddvallem  13703  xpsaddlem  13727  xpsvsca  13731  mrcun  13774  homfeqval  13850  comfeqval  13861  sectcan  13908  sectco  13909  sectmon  13930  monsect  13931  funcsect  13996  setcmon  14169  resscatc  14187  catciso  14189  evlfcllem  14245  curf2cl  14255  curfcl  14256  yonedalem4c  14301  yonedalem3b  14303  yonedainv  14305  latj12  14452  mnd12g  14627  resmhm  14686  pwsco2mhm  14697  frmdup3  14738  grprcan  14765  grplcan  14784  grpinv11  14787  grpinvnz  14789  grplmulf1o  14792  grpinvpropd  14793  grpinvadd  14794  grpsubsub4  14808  mulgz  14838  mulgdirlem  14841  mulgdir  14842  mulgass  14847  mulgsubdir  14848  mulgpropd  14850  pwsmulg  14859  imasgrp2  14860  isnsg3  14901  nmzsubg  14908  ssnmz  14909  eqger  14917  eqglact  14918  ghminv  14940  conjnmz  14966  subgga  15004  gasubg  15006  galcan  15008  gacan  15009  cntzsubg  15062  cntzmhm  15064  sylow1lem1  15159  sylow2blem2  15182  sylow2blem3  15183  lsmmod  15234  lsmpropd  15236  lsmdisj2  15241  subgdisj1  15250  subgdisj2  15251  efgredleme  15302  efgredlemd  15303  efgredlemc  15304  efgredlem  15306  frgpup3lem  15336  mulgdi  15376  lsm4  15402  cygabl  15427  gsummhm2  15462  gsumpt  15472  gsum2d  15473  dprdfeq0  15507  ablfac1eu  15558  rngcom  15619  isrngd  15625  rnglz  15627  rngrz  15628  rng1eq0  15629  rngmneg1  15632  gsumdixp  15642  unitgrp  15699  irredrmul  15739  drngmul0or  15783  subrginv  15811  subrgunit  15813  srngnvl  15871  srngadd  15872  srngmul  15873  issrngd  15876  lmodvs0  15911  lmodvneg1  15914  lmodcom  15917  lmodsubdi  15928  lmodvsinv  16039  lmodvsinv2  16040  lmhmvsca  16048  lvecvs0or  16107  lvecinv  16112  lspsnvs  16113  lspabs2  16119  lspfixed  16127  lspsolv  16142  unitrrg  16280  asclpropd  16331  psrass1lem  16369  psrlidm  16394  psrridm  16395  mvrf1  16416  mplmon2mul  16488  coe1pwmul  16598  prmirredlem  16696  mulgrhm2  16711  chrrhm  16735  znidomb  16765  ip0r  16791  ipdir  16793  ipdi  16794  ipass  16799  ipassr  16800  phlpropd  16809  ocvpj  16867  restin  17152  cncmp  17377  cmpsublem  17384  conndisj  17400  cnconn  17406  kgencmp2  17499  ufldom  17915  tgplacthmeo  18054  ghmcnp  18065  divstgpopn  18070  divstgphaus  18073  tsmsxplem2  18104  tususp  18223  xpsdsval  18319  blpnfctr  18356  xmssym  18385  ressxms  18445  isngp2  18515  ngppropd  18549  nminvr  18576  blcvx  18700  icccvx  18846  pcohtpylem  18915  pcohtpy  18916  pjthlem1  19205  ovollb2lem  19251  ovolicc2lem1  19280  ovolicc2lem5  19284  volsup  19317  ovolioo  19329  uniiccdif  19337  uniioombllem3  19344  uniioombllem4  19345  vitalilem3  19369  itg1sub  19468  itg2const  19499  iblcnlem1  19546  itgcnlem  19548  itgaddlem2  19582  itgsub  19584  itgabs  19593  ditgsplit  19615  dvmulbr  19692  dvcmul  19697  dvcmulf  19698  dvrec  19708  dvmptres3  19709  dvmptadd  19713  dvmptmul  19714  dvmptres2  19715  dvmptneg  19719  dvmptsub  19720  dvmptcj  19721  dvmptco  19725  dveflem  19730  dvlip  19744  dvlipcn  19745  dvlip2  19746  dvcvx  19771  dvfsumle  19772  dvfsumabs  19774  dvfsumlem1  19777  dvfsumlem2  19778  ftc2  19795  ftc2ditglem  19796  itgparts  19798  itgsubstlem  19799  itgsubst  19800  evlslem1  19803  evlseu  19804  evlssca  19810  evlsvar  19811  pf1ind  19842  fta1glem1  19955  fta1blem  19958  plyeq0lem  19996  plymullem1  20000  coeeulem  20010  coe0  20041  coesub  20042  dvply1  20068  plydivlem4  20080  plyrem  20089  fta1lem  20091  vieta1  20096  plyexmo  20097  elqaalem2  20104  aareccl  20110  aannenlem1  20112  aaliou3lem2  20127  dvtaylp  20153  taylthlem1  20156  radcnvlem1  20196  pserdvlem2  20211  efcvx  20232  ptolemy  20271  tangtx  20280  efif1olem3  20313  efif1olem4  20314  lognegb  20351  efiarg  20369  cosargd  20370  tanarg  20381  logtayl  20418  cxpsub  20440  cxproot  20448  cxpsqr  20461  cxpcn3lem  20498  cxpaddlelem  20502  abscxpbnd  20504  root1eq1  20506  cxpeq  20508  logrec  20528  isosctrlem2  20530  isosctrlem3  20531  isosctr  20532  ssscongptld  20533  chordthmlem  20540  quad2  20546  dcubic1lem  20550  mcubic  20554  cubic2  20555  cubic  20556  dquartlem2  20559  dquart  20560  quart1lem  20562  quart1  20563  asinlem2  20576  asinlem3  20578  asinsin  20599  sinacos  20612  atanlogsublem  20622  efiatan2  20624  2efiatan  20625  tanatan  20626  atantan  20630  atans2  20638  dvatan  20642  atantayl  20644  atantayl2  20645  log2cnv  20651  rlimcnp2  20672  cxplim  20677  cxp2lim  20682  cvxcl  20690  scvxcvx  20691  wilthlem1  20718  wilthlem2  20719  ftalem5  20726  basellem3  20732  basellem5  20734  basellem8  20737  mumullem2  20830  musum  20843  musumsum  20844  muinv  20845  sgmppw  20848  1sgmprm  20850  1sgm2ppw  20851  ppiub  20855  logfac2  20868  chpchtsum  20870  perfectlem1  20880  perfectlem2  20881  dchrn0  20901  dchrfi  20906  dchrabs  20911  dchrptlem1  20915  dchrhash  20922  dchr2sum  20924  sum2dchr  20925  bposlem6  20940  bposlem9  20943  lgsvalmod  20966  lgsdilem  20973  lgsne0  20984  lgssq  20986  lgssq2  20987  lgsqr  20997  lgsdchrval  20998  lgsdchr  20999  lgseisenlem1  21000  lgseisenlem2  21001  lgseisenlem4  21003  lgsquadlem1  21005  lgsquadlem3  21007  lgsquad3  21012  m1lgs  21013  rplogsumlem1  21045  rplogsumlem2  21046  dchrisumlem2  21051  dchrisum0fno1  21072  rpvmasum2  21073  dchrisum0lem1  21077  dchrisum0lem2  21079  mudivsum  21091  mulog2sumlem1  21095  vmalogdivsum  21100  2vmadivsumlem  21101  logsqvma  21103  selberglem2  21107  selberg2lem  21111  selberg3lem1  21118  selberg4lem1  21121  selberg4  21122  pntrsumo1  21126  selbergr  21129  selberg34r  21132  pntrlog2bndlem3  21140  pntrlog2bndlem4  21141  pntibndlem2  21152  pntlemg  21159  pntlemr  21163  pntlemf  21166  ostthlem1  21188  padicabvcxp  21193  ostth3  21199  cusgrasizeindslem3  21350  grpoidinvlem1  21640  grpoideu  21645  grporcan  21657  grpolcan  21669  grpoasscan1  21673  grpoinvop  21677  grpopnpcan2  21689  gxsuc  21708  gxsub  21712  gxmul  21714  ablo4  21723  subgoinv  21744  ablomul  21791  ghgrp  21804  ghablo  21805  rngolz  21837  rngorz  21838  zerdivemp1  21870  nvadd12  21950  nvscom  21958  nvmul0or  21981  nvz0  22005  smcnlem  22041  ipidsq  22057  sspz  22082  lno0  22105  lnoadd  22107  lnomul  22109  ipasslem3  22182  dipdi  22192  dipassr  22195  dipsubdi  22198  ubthlem2  22221  hvmul0or  22375  hvadd12  22385  hvadd4  22386  hvmulcom  22393  normneg  22494  pjhthlem1  22741  chj12  22884  spanunsni  22929  5oalem2  23005  3oalem2  23013  mayete3iOLD  23079  hoadd4  23135  homul12  23156  hosubdi  23159  honegsubdi  23161  hosub4  23164  adj2  23285  lnopmul  23318  lnopaddi  23322  lnfnaddi  23394  lnfnmuli  23395  cnlnadjlem6  23423  adjeq0  23442  leopmul  23485  opsqrlem1  23491  opsqrlem6  23496  hstnmoc  23574  strlem1  23601  chirredlem3  23743  bcm1n  23987  divnumden2  23999  xmulcand  24005  xreceu  24006  xaddeq0  24030  xrsmulgzz  24033  xrge0adddir  24044  dvrcan5  24058  ofldaddlt  24067  rhmunitinv  24076  qqhval2lem  24164  esummulc1  24267  measxun2  24358  measssd  24363  totprobd  24463  zetacvg  24578  lgamgulmlem4  24595  lgamcvg2  24618  gamp1  24621  subfaclim  24653  cvxscon  24709  rescon  24712  cvmliftmolem1  24747  cvmliftlem7  24757  cvmliftlem13  24762  cvmlift2lem7  24775  cvmlift3lem5  24789  ghomf1olem  24884  fprodm1  25069  fallfacfwd  25119  faclim2  25125  funsseq  25149  brbtwn2  25558  axsegconlem10  25579  ax5seglem3  25584  ax5seglem6  25587  axpaschlem  25593  axeuclidlem  25615  axcontlem2  25618  axcontlem7  25623  axcontlem8  25624  bpolydiflem  25814  bpoly4  25819  fsumcube  25820  itg2addnclem  25957  itg2addnc  25959  itgaddnclem2  25964  itgsubnc  25967  iblmulc2nc  25970  itgabsnc  25974  areacirclem2  25982  areacirclem5  25986  areacirc  25988  clsun  26022  topjoin  26085  cocanfo  26110  ablo4pnp  26246  zerdivemp1x  26262  crngm4  26304  crngohomfo  26307  diophrw  26508  eldioph2lem1  26509  pellexlem2  26584  pellexlem6  26588  pellex  26589  pell1234qrne0  26607  pell1234qrreccl  26608  pell1qrgaplem  26627  rmxm1  26688  oddcomabszz  26698  jm2.19lem1  26751  jm3.1lem2  26780  dnnumch3  26813  pwssplit4  26860  uvcresum  26911  lmimlbs  26975  flcidc  27048  psgnunilem2  27087  psgnghm  27106  gsumcom3  27123  hashgcdlem  27185  deg1mhm  27195  dvsconst  27216  dvsid  27217  expgrowth  27221  itgsinexplem1  27416  itgsinexp  27417  stoweidlem1  27418  wallispi2lem2  27489  stirlinglem3  27493  stirlinglem5  27495  stirlinglem10  27500  stirlinglem15  27505  sigaradd  27524  cevathlem1  27525  frgrancvvdeq  27794  frgrancvvdgeq  27795  bnj1379  28540  bnj1321  28734  lfl0  29180  lfladd  29181  lflmul  29183  eqlkr3  29216  olm11  29342  latm12  29345  cmtcomlemN  29363  omlspjN  29376  hlatj12  29485  1cvrjat  29589  dalemrotyz  29772  padd12N  29953  pmapjlln1  29969  atmod2i1  29975  pmapocjN  30044  pnonsingN  30047  pexmidN  30083  lhp2at0  30146  lhpelim  30151  ltrncnv  30260  ltrnmw  30265  cdleme7c  30359  cdleme15b  30389  cdlemednpq  30413  cdleme20y  30416  cdleme20m  30437  cdleme22cN  30456  cdleme22d  30457  cdleme23b  30464  cdleme30a  30492  cdleme35h  30570  cdlemeg46frv  30639  cdlemg2fv2  30714  cdlemg2l  30717  cdlemg2m  30718  cdlemg8c  30743  cdlemg10bALTN  30750  cdlemg12  30764  cdlemg13a  30765  cdlemg18c  30794  cdlemg19  30798  trlcoat  30837  cdlemg47  30850  tendo1ne0  30942  cdlemk9  30953  cdlemk9bN  30954  dia2dimlem1  31179  tendolinv  31220  tendorinv  31221  dvhlveclem  31223  doca3N  31242  dihmeetlem7N  31425  dihjatc1  31426  dihmeetlem18N  31439  dochnoncon  31506  dihjatc  31532  dihjatcclem1  31533  dihjatcclem4  31536  dochsnkr  31587  lcfl7lem  31614  lcfl8  31617  lcfl9a  31620  lclkrlem1  31621  lclkrlem2e  31626  lclkrlem2j  31631  lcfrlem1  31657  lcfrlem9  31665  lcfrlem23  31680  lcfrlem31  31688  mapd0  31780  mapdpglem21  31807  baerlem3lem1  31822  baerlem5alem1  31823  mapdindp4  31838  mapdh6gN  31857  hdmap1l6g  31932  hgmapval0  32010  hgmaprnlem1N  32014  hlhilhillem  32078
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2380
  Copyright terms: Public domain W3C validator