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

Theorem 3eqtr3d 2475
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 2469 . 2  |-  ( ph  ->  B  =  C )
4 3eqtr3d.3 . 2  |-  ( ph  ->  B  =  D )
53, 4eqtr3d 2469 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652
This theorem is referenced by:  mpteqb  5811  fvmptt  5812  fsnunfv  5925  f1ocnvfv1  6006  f1ocnvfv2  6007  fcof1  6012  weniso  6067  caov12d  6260  caov13d  6262  caov411d  6264  caovmo  6276  grprinvlem  6277  grprinvd  6278  grpridd  6279  onovuni  6596  seqomlem1  6699  seqomlem4  6702  onasuc  6764  onesuc  6766  oeeui  6837  fopwdom  7208  unxpdomlem2  7306  cantnfres  7625  cnfcom2lem  7650  cnfcom2  7651  cardiun  7861  ackbij1lem16  8107  ackbij2lem2  8112  fpwwe2lem6  8502  fpwwe2lem8  8504  canthp1lem2  8520  mul12  9224  mul4  9227  addid1  9238  addcan  9242  addcom  9244  addcomd  9260  add12  9271  ppncan  9335  addsub4  9336  muladd  9458  mulcand  9647  receu  9659  div13  9691  divdivdiv  9707  divcan5  9708  divdiv1  9717  divdiv2  9718  halfaddsub  10193  uzindOLD  10356  xadddi  10866  xov1plusxeqvd  11033  fztp  11094  flzadd  11220  fldiv  11233  modnegd  11273  modsub12d  11275  seqm1  11332  seqcaopr  11352  seqf1o  11356  expsub  11419  zesq  11494  digit1  11505  discr1  11507  discr  11508  facnn2  11567  faclbnd6  11582  hashfz1  11622  hashdom  11645  hashun  11648  hashbclem  11693  hashfac  11699  seqcoll  11704  ccatopth  11768  shftval3  11883  crre  11911  resub  11924  imsub  11932  cjsub  11946  abslem2  12135  sqreulem  12155  climshft2  12368  isercolllem2  12451  iseraltlem2  12468  iseraltlem3  12469  fsumsub  12563  fsumtscopo  12573  fsumtscopo2  12574  hashiun  12593  bcxmas  12607  climcndslem1  12621  climcndslem2  12622  trireciplem  12633  geoser  12638  geo2sum2  12643  sinsub  12761  cossub  12762  rpnnen2lem10  12815  ruclem12  12832  divalglem9  12913  bitsinv1lem  12945  bitsinv1  12946  bitsf1  12950  sadasslem  12974  bitsres  12977  smup1  12993  smumul  12997  modgcd  13028  absmulgcd  13039  gcdmultiplez  13043  eucalg  13070  numdensq  13138  dfphi2  13155  phiprm  13158  fermltl  13165  prmdiveq  13167  odzdvds  13173  coprimeprodsq  13175  pythagtriplem6  13187  pythagtriplem7  13188  pythagtriplem12  13192  pythagtriplem16  13196  pcaddlem  13249  sumhash  13257  pcfac  13260  pockthlem  13265  prmreclem6  13281  4sqlem12  13316  4sqlem15  13319  vdwlem3  13343  vdwlem6  13346  vdwlem9  13349  ramub1lem2  13387  divsaddvallem  13768  xpsaddlem  13792  xpsvsca  13796  mrcun  13839  homfeqval  13915  comfeqval  13926  sectcan  13973  sectco  13974  sectmon  13995  monsect  13996  funcsect  14061  setcmon  14234  resscatc  14252  catciso  14254  evlfcllem  14310  curf2cl  14320  curfcl  14321  yonedalem4c  14366  yonedalem3b  14368  yonedainv  14370  latj12  14517  mnd12g  14692  resmhm  14751  pwsco2mhm  14762  frmdup3  14803  grprcan  14830  grplcan  14849  grpinv11  14852  grpinvnz  14854  grplmulf1o  14857  grpinvpropd  14858  grpinvadd  14859  grpsubsub4  14873  mulgz  14903  mulgdirlem  14906  mulgdir  14907  mulgass  14912  mulgsubdir  14913  mulgpropd  14915  pwsmulg  14924  imasgrp2  14925  isnsg3  14966  nmzsubg  14973  ssnmz  14974  eqger  14982  eqglact  14983  ghminv  15005  conjnmz  15031  subgga  15069  gasubg  15071  galcan  15073  gacan  15074  cntzsubg  15127  cntzmhm  15129  sylow1lem1  15224  sylow2blem2  15247  sylow2blem3  15248  lsmmod  15299  lsmpropd  15301  lsmdisj2  15306  subgdisj1  15315  subgdisj2  15316  efgredleme  15367  efgredlemd  15368  efgredlemc  15369  efgredlem  15371  frgpup3lem  15401  mulgdi  15441  lsm4  15467  cygabl  15492  gsummhm2  15527  gsumpt  15537  gsum2d  15538  dprdfeq0  15572  ablfac1eu  15623  rngcom  15684  isrngd  15690  rnglz  15692  rngrz  15693  rng1eq0  15694  rngmneg1  15697  gsumdixp  15707  unitgrp  15764  irredrmul  15804  drngmul0or  15848  subrginv  15876  subrgunit  15878  srngnvl  15936  srngadd  15937  srngmul  15938  issrngd  15941  lmodvs0  15976  lmodvneg1  15979  lmodcom  15982  lmodsubdi  15993  lmodvsinv  16104  lmodvsinv2  16105  lmhmvsca  16113  lvecvs0or  16172  lvecinv  16177  lspsnvs  16178  lspabs2  16184  lspfixed  16192  lspsolv  16207  unitrrg  16345  asclpropd  16396  psrass1lem  16434  psrlidm  16459  psrridm  16460  mvrf1  16481  mplmon2mul  16553  coe1pwmul  16663  prmirredlem  16765  mulgrhm2  16780  chrrhm  16804  znidomb  16834  ip0r  16860  ipdir  16862  ipdi  16863  ipass  16868  ipassr  16869  phlpropd  16878  ocvpj  16936  restin  17222  cncmp  17447  cmpsublem  17454  conndisj  17471  cnconn  17477  kgencmp2  17570  ufldom  17986  tgplacthmeo  18125  ghmcnp  18136  divstgpopn  18141  divstgphaus  18144  tsmsxplem2  18175  tususp  18294  xpsdsval  18403  blpnfctr  18458  xmssym  18487  ressxms  18547  isngp2  18636  ngppropd  18670  nminvr  18697  blcvx  18821  icccvx  18967  pcohtpylem  19036  pcohtpy  19037  pjthlem1  19330  ovollb2lem  19376  ovolicc2lem1  19405  ovolicc2lem5  19409  volsup  19442  ovolioo  19454  uniiccdif  19462  uniioombllem3  19469  uniioombllem4  19470  vitalilem3  19494  itg1sub  19593  itg2const  19624  iblcnlem1  19671  itgcnlem  19673  itgaddlem2  19707  itgsub  19709  itgabs  19718  ditgsplit  19740  dvmulbr  19817  dvcmul  19822  dvcmulf  19823  dvrec  19833  dvmptres3  19834  dvmptadd  19838  dvmptmul  19839  dvmptres2  19840  dvmptneg  19844  dvmptsub  19845  dvmptcj  19846  dvmptco  19850  dveflem  19855  dvlip  19869  dvlipcn  19870  dvlip2  19871  dvcvx  19896  dvfsumle  19897  dvfsumabs  19899  dvfsumlem1  19902  dvfsumlem2  19903  ftc2  19920  ftc2ditglem  19921  itgparts  19923  itgsubstlem  19924  itgsubst  19925  evlslem1  19928  evlseu  19929  evlssca  19935  evlsvar  19936  pf1ind  19967  fta1glem1  20080  fta1blem  20083  plyeq0lem  20121  plymullem1  20125  coeeulem  20135  coe0  20166  coesub  20167  dvply1  20193  plydivlem4  20205  plyrem  20214  fta1lem  20216  vieta1  20221  plyexmo  20222  elqaalem2  20229  aareccl  20235  aannenlem1  20237  aaliou3lem2  20252  dvtaylp  20278  taylthlem1  20281  radcnvlem1  20321  pserdvlem2  20336  efcvx  20357  ptolemy  20396  tangtx  20405  efif1olem3  20438  efif1olem4  20439  lognegb  20476  efiarg  20494  cosargd  20495  tanarg  20506  logtayl  20543  cxpsub  20565  cxproot  20573  cxpsqr  20586  cxpcn3lem  20623  cxpaddlelem  20627  abscxpbnd  20629  root1eq1  20631  cxpeq  20633  logrec  20653  isosctrlem2  20655  isosctrlem3  20656  isosctr  20657  ssscongptld  20658  chordthmlem  20665  quad2  20671  dcubic1lem  20675  mcubic  20679  cubic2  20680  cubic  20681  dquartlem2  20684  dquart  20685  quart1lem  20687  quart1  20688  asinlem2  20701  asinlem3  20703  asinsin  20724  sinacos  20737  atanlogsublem  20747  efiatan2  20749  2efiatan  20750  tanatan  20751  atantan  20755  atans2  20763  dvatan  20767  atantayl  20769  atantayl2  20770  log2cnv  20776  rlimcnp2  20797  cxplim  20802  cxp2lim  20807  cvxcl  20815  scvxcvx  20816  wilthlem1  20843  wilthlem2  20844  ftalem5  20851  basellem3  20857  basellem5  20859  basellem8  20862  mumullem2  20955  musum  20968  musumsum  20969  muinv  20970  sgmppw  20973  1sgmprm  20975  1sgm2ppw  20976  ppiub  20980  logfac2  20993  chpchtsum  20995  perfectlem1  21005  perfectlem2  21006  dchrn0  21026  dchrfi  21031  dchrabs  21036  dchrptlem1  21040  dchrhash  21047  dchr2sum  21049  sum2dchr  21050  bposlem6  21065  bposlem9  21068  lgsvalmod  21091  lgsdilem  21098  lgsne0  21109  lgssq  21111  lgssq2  21112  lgsqr  21122  lgsdchrval  21123  lgsdchr  21124  lgseisenlem1  21125  lgseisenlem2  21126  lgseisenlem4  21128  lgsquadlem1  21130  lgsquadlem3  21132  lgsquad3  21137  m1lgs  21138  rplogsumlem1  21170  rplogsumlem2  21171  dchrisumlem2  21176  dchrisum0fno1  21197  rpvmasum2  21198  dchrisum0lem1  21202  dchrisum0lem2  21204  mudivsum  21216  mulog2sumlem1  21220  vmalogdivsum  21225  2vmadivsumlem  21226  logsqvma  21228  selberglem2  21232  selberg2lem  21236  selberg3lem1  21243  selberg4lem1  21246  selberg4  21247  pntrsumo1  21251  selbergr  21254  selberg34r  21257  pntrlog2bndlem3  21265  pntrlog2bndlem4  21266  pntibndlem2  21277  pntlemg  21284  pntlemr  21288  pntlemf  21291  ostthlem1  21313  padicabvcxp  21318  ostth3  21324  cusgrasizeindslem3  21476  grpoidinvlem1  21784  grpoideu  21789  grporcan  21801  grpolcan  21813  grpoasscan1  21817  grpoinvop  21821  grpopnpcan2  21833  gxsuc  21852  gxsub  21856  gxmul  21858  ablo4  21867  subgoinv  21888  ablomul  21935  ghgrp  21948  ghablo  21949  rngolz  21981  rngorz  21982  zerdivemp1  22014  nvadd12  22094  nvscom  22102  nvmul0or  22125  nvz0  22149  smcnlem  22185  ipidsq  22201  sspz  22226  lno0  22249  lnoadd  22251  lnomul  22253  ipasslem3  22326  dipdi  22336  dipassr  22339  dipsubdi  22342  ubthlem2  22365  hvmul0or  22519  hvadd12  22529  hvadd4  22530  hvmulcom  22537  normneg  22638  pjhthlem1  22885  chj12  23028  spanunsni  23073  5oalem2  23149  3oalem2  23157  mayete3iOLD  23223  hoadd4  23279  homul12  23300  hosubdi  23303  honegsubdi  23305  hosub4  23308  adj2  23429  lnopmul  23462  lnopaddi  23466  lnfnaddi  23538  lnfnmuli  23539  cnlnadjlem6  23567  adjeq0  23586  leopmul  23629  opsqrlem1  23635  opsqrlem6  23640  hstnmoc  23718  strlem1  23745  chirredlem3  23887  xaddeq0  24111  bcm1n  24143  divnumden2  24153  xmulcand  24159  xreceu  24160  xrsmulgzz  24192  xrge0adddir  24207  dvrcan5  24221  ofldaddlt  24233  rhmunitinv  24252  qqhval2lem  24357  esummulc1  24463  measxun2  24556  measssd  24561  totprobd  24676  zetacvg  24791  lgamgulmlem4  24808  lgamcvg2  24831  gamp1  24834  subfaclim  24866  cvxscon  24922  rescon  24925  cvmliftmolem1  24960  cvmliftlem7  24970  cvmliftlem13  24975  cvmlift2lem7  24988  cvmlift3lem5  25002  ghomf1olem  25097  fprodm1  25282  fallfacfwd  25344  binomfallfaclem2  25348  faclim2  25359  funsseq  25385  brbtwn2  25836  axsegconlem10  25857  ax5seglem3  25862  ax5seglem6  25865  axpaschlem  25871  axeuclidlem  25893  axcontlem2  25896  axcontlem7  25901  axcontlem8  25902  bpolydiflem  26092  bpoly4  26097  fsumcube  26098  itg2addnclem  26246  itg2addnclem3  26248  itgaddnclem2  26254  itgsubnc  26257  iblmulc2nc  26260  itgabsnc  26264  ftc2nc  26279  areacirclem2  26282  areacirclem5  26286  areacirc  26288  clsun  26322  topjoin  26385  cocanfo  26410  ablo4pnp  26546  zerdivemp1x  26562  crngm4  26604  crngohomfo  26607  diophrw  26808  eldioph2lem1  26809  pellexlem2  26884  pellexlem6  26888  pellex  26889  pell1234qrne0  26907  pell1234qrreccl  26908  pell1qrgaplem  26927  rmxm1  26988  oddcomabszz  26998  jm2.19lem1  27051  jm3.1lem2  27080  dnnumch3  27113  pwssplit4  27159  uvcresum  27210  lmimlbs  27274  flcidc  27347  psgnunilem2  27386  psgnghm  27405  gsumcom3  27422  hashgcdlem  27484  deg1mhm  27494  dvsconst  27515  dvsid  27516  expgrowth  27520  itgsinexplem1  27715  itgsinexp  27716  stoweidlem1  27717  wallispi2lem2  27788  stirlinglem3  27792  stirlinglem5  27794  stirlinglem10  27799  stirlinglem15  27804  sigaradd  27823  cevathlem1  27824  imarnf1pr  28070  2submod  28130  modprm0  28194  cshwssizelem4a  28246  frgrancvvdeq  28368  frgrancvvdgeq  28369  bnj1379  29139  bnj1321  29333  lfl0  29800  lfladd  29801  lflmul  29803  eqlkr3  29836  olm11  29962  latm12  29965  cmtcomlemN  29983  omlspjN  29996  hlatj12  30105  1cvrjat  30209  dalemrotyz  30392  padd12N  30573  pmapjlln1  30589  atmod2i1  30595  pmapocjN  30664  pnonsingN  30667  pexmidN  30703  lhp2at0  30766  lhpelim  30771  ltrncnv  30880  ltrnmw  30885  cdleme7c  30979  cdleme15b  31009  cdlemednpq  31033  cdleme20y  31036  cdleme20m  31057  cdleme22cN  31076  cdleme22d  31077  cdleme23b  31084  cdleme30a  31112  cdleme35h  31190  cdlemeg46frv  31259  cdlemg2fv2  31334  cdlemg2l  31337  cdlemg2m  31338  cdlemg8c  31363  cdlemg10bALTN  31370  cdlemg12  31384  cdlemg13a  31385  cdlemg18c  31414  cdlemg19  31418  trlcoat  31457  cdlemg47  31470  tendo1ne0  31562  cdlemk9  31573  cdlemk9bN  31574  dia2dimlem1  31799  tendolinv  31840  tendorinv  31841  dvhlveclem  31843  doca3N  31862  dihmeetlem7N  32045  dihjatc1  32046  dihmeetlem18N  32059  dochnoncon  32126  dihjatc  32152  dihjatcclem1  32153  dihjatcclem4  32156  dochsnkr  32207  lcfl7lem  32234  lcfl8  32237  lcfl9a  32240  lclkrlem1  32241  lclkrlem2e  32246  lclkrlem2j  32251  lcfrlem1  32277  lcfrlem9  32285  lcfrlem23  32300  lcfrlem31  32308  mapd0  32400  mapdpglem21  32427  baerlem3lem1  32442  baerlem5alem1  32443  mapdindp4  32458  mapdh6gN  32477  hdmap1l6g  32552  hgmapval0  32630  hgmaprnlem1N  32634  hlhilhillem  32698
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-cleq 2428
  Copyright terms: Public domain W3C validator