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

Theorem 3eqtr3d 2693
 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 (𝜑𝐴 = 𝐵)
3eqtr3d.2 (𝜑𝐴 = 𝐶)
3eqtr3d.3 (𝜑𝐵 = 𝐷)
Assertion
Ref Expression
3eqtr3d (𝜑𝐶 = 𝐷)

Proof of Theorem 3eqtr3d
StepHypRef Expression
1 3eqtr3d.1 . . 3 (𝜑𝐴 = 𝐵)
2 3eqtr3d.2 . . 3 (𝜑𝐴 = 𝐶)
31, 2eqtr3d 2687 . 2 (𝜑𝐵 = 𝐶)
4 3eqtr3d.3 . 2 (𝜑𝐵 = 𝐷)
53, 4eqtr3d 2687 1 (𝜑𝐶 = 𝐷)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1523 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631 This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644 This theorem is referenced by:  mpteqb  6338  fvmptt  6339  fsnunfv  6494  f1ocnvfv1  6572  f1ocnvfv2  6573  fcof1  6582  weniso  6644  caov12d  6897  caov13d  6899  caov411d  6901  caovmo  6913  grprinvlem  6914  grprinvd  6915  grpridd  6916  onovuni  7484  tfrlem5  7521  seqomlem1  7590  seqomlem4  7593  onasuc  7653  onesuc  7655  oeeui  7727  fopwdom  8109  unxpdomlem2  8206  cantnfres  8612  cnfcom2lem  8636  cnfcom2  8637  cardiun  8846  ackbij1lem16  9095  ackbij2lem2  9100  fpwwe2lem6  9495  fpwwe2lem8  9497  canthp1lem2  9513  mul12  10240  mul4  10243  addid1  10254  addcan  10258  addcom  10260  addcomd  10276  add12  10291  ppncan  10361  addsub4  10362  subaddeqd  10484  muladd  10500  mulcand  10698  receu  10710  div13  10744  divdivdiv  10764  divcan5  10765  divdiv1  10774  divdiv2  10775  halfaddsub  11303  xadddi  12163  xov1plusxeqvd  12356  fztp  12435  flzadd  12667  fldiv  12699  mulp1mod1  12751  modnegd  12765  modsub12d  12767  2submod  12771  seqm1  12858  seqcaopr  12878  seqf1o  12882  exprec  12941  expsub  12948  zesq  13027  digit1  13038  discr1  13040  discr  13041  facnn2  13109  faclbnd6  13126  hashfz1  13174  hashdom  13206  hashun  13209  hashbclem  13274  hashfac  13280  seqcoll  13286  ccatopth  13516  repsw2  13739  repsw3  13740  shftval3  13860  crre  13898  resub  13911  imsub  13919  cjsub  13933  abslem2  14123  sqreulem  14143  climshft2  14357  isercolllem2  14440  iseraltlem2  14457  iseraltlem3  14458  fsumsub  14564  telfsumo  14578  telfsumo2  14579  hashiun  14598  bcxmas  14611  climcndslem1  14625  climcndslem2  14626  trireciplem  14638  geoser  14643  geo2sum2  14649  fprodm1  14741  fallfacfwd  14811  binomfallfaclem2  14815  bpolydiflem  14829  bpoly4  14834  fsumcube  14835  sinsub  14942  cossub  14943  rpnnen2lem10  14996  ruclem12  15014  p1modz1  15034  mod2eq1n2dvds  15118  pwp1fsum  15161  divalglem9  15171  bitsinv1lem  15210  bitsinv1  15211  bitsf1  15215  sadasslem  15239  bitsres  15242  smup1  15258  smumul  15262  modgcd  15300  absmulgcd  15313  gcdmultiplez  15317  eucalg  15347  lcmgcd  15367  lcmid  15369  lcmftp  15396  numdensq  15509  dfphi2  15526  phiprm  15529  fermltl  15536  prmdiveq  15538  hashgcdlem  15540  odzdvds  15547  powm2modprm  15555  modprm0  15557  coprimeprodsq  15560  pythagtriplem6  15573  pythagtriplem7  15574  pythagtriplem12  15578  pythagtriplem16  15582  pcaddlem  15639  sumhash  15647  pcfac  15650  pockthlem  15656  prmreclem6  15672  4sqlem12  15707  4sqlem15  15710  vdwlem3  15734  vdwlem6  15737  vdwlem9  15740  ramub1lem2  15778  cshwshashlem2  15850  qusaddvallem  16258  xpsaddlem  16282  xpsvsca  16286  mrcun  16329  homfeqval  16404  comfeqval  16415  sectcan  16462  sectco  16463  sectmon  16489  monsect  16490  funcsect  16579  setcmon  16784  resscatc  16802  catciso  16804  evlfcllem  16908  curf2cl  16918  curfcl  16919  yonedalem4c  16964  yonedalem3b  16966  yonedainv  16968  latj12  17143  mnd12g  17353  resmhm  17406  pwsco2mhm  17418  frmdup3lem  17450  grprcan  17502  grplcan  17524  grpasscan1  17525  grpinv11  17531  grpinvnz  17533  grplmulf1o  17536  grpinvpropd  17537  grpinvadd  17540  grpsubsub4  17555  dfgrp3  17561  imasgrp2  17577  mhmid  17583  mhmmnd  17584  mulgz  17615  mulgdirlem  17619  mulgdir  17620  mulgass  17626  mulgsubdir  17629  mulgpropd  17631  pwsmulg  17634  isnsg3  17675  nmzsubg  17682  ssnmz  17683  eqger  17691  eqglact  17692  ghminv  17714  conjnmz  17741  subgga  17779  gasubg  17781  galcan  17783  gacan  17784  cntzsubg  17815  cntzmhm  17817  psgnunilem2  17961  sylow1lem1  18059  sylow2blem2  18082  sylow2blem3  18083  lsmmod  18134  lsmpropd  18136  lsmdisj2  18141  subgdisj1  18150  subgdisj2  18151  efgredleme  18202  efgredlemd  18203  efgredlemc  18204  efgredlem  18206  frgpup3lem  18236  mulgdi  18278  ghmcmn  18283  lsm4  18309  cygabl  18338  gsummhm2  18385  gsumpt  18407  gsum2d  18417  dprdfeq0  18467  ablfac1eu  18518  ringcom  18625  isringd  18631  ringlz  18633  ringrz  18634  ring1eq0  18636  ringmneg1  18642  gsumdixp  18655  unitgrp  18713  irredrmul  18753  drngmul0or  18816  subrginv  18844  subrgunit  18846  abvrec  18884  srngnvl  18904  srngadd  18905  srngmul  18906  issrngd  18909  lmodvs0  18945  lmodvneg1  18954  lmodcom  18957  lmodsubdi  18968  lmodvsinv  19084  lmodvsinv2  19085  lmhmvsca  19093  lvecvs0or  19156  lvecinv  19161  lspsnvs  19162  lspabs2  19168  lspfixed  19176  lspsolv  19191  unitrrg  19341  asclpropd  19394  psrass1lem  19425  psrlidm  19451  psrridm  19452  mvrf1  19473  mplmon2mul  19549  evlslem1  19563  evlseu  19564  evlssca  19570  evlsvar  19571  coe1pwmul  19697  pf1ind  19767  prmirredlem  19889  mulgrhm2  19895  chrrhm  19927  znidomb  19958  psgnghm  19974  psgninv  19976  zrhpsgnodpm  19986  evpmodpmf1o  19990  psgndiflemB  19994  ip0r  20030  ipdir  20032  ipdi  20033  ipass  20038  ipassr  20039  phlpropd  20048  ocvpj  20109  uvcresum  20180  lmimlbs  20223  gsumcom3  20253  mat0dimbas0  20320  mdetrlin  20456  mdetrsca  20457  mdetr0  20459  mdetunilem8  20473  mdetuni0  20475  mdetmul  20477  maducoeval2  20494  madurid  20498  madulid  20499  matinv  20531  matunit  20532  slesolinv  20534  slesolinvbi  20535  cpmadugsumlemF  20729  restin  21018  cncmp  21243  cmpsublem  21250  conndisj  21267  cnconn  21273  kgencmp2  21397  ufldom  21813  tgplacthmeo  21954  ghmcnp  21965  qustgpopn  21970  qustgphaus  21973  tsmsxplem2  22004  tususp  22123  xpsdsval  22233  blpnfctr  22288  xmssym  22317  ressxms  22377  isngp2  22448  ngppropd  22488  nminvr  22520  blcvx  22648  icccvx  22796  pcohtpylem  22865  pcohtpy  22866  clmvscom  22936  cvsmuleqdivd  22980  cvsdiveqd  22981  pjthlem1  23254  ovollb2lem  23302  ovolicc2lem1  23331  ovolicc2lem5  23335  volsup  23370  ovolioo  23382  uniiccdif  23392  uniioombllem3  23399  uniioombllem4  23400  vitalilem3  23424  itg1sub  23521  itg2const  23552  iblcnlem1  23599  itgcnlem  23601  itgaddlem2  23635  itgsub  23637  itgabs  23646  ditgsplit  23670  dvmulbr  23747  dvcmul  23752  dvcmulf  23753  dvrec  23763  dvmptres3  23764  dvmptadd  23768  dvmptmul  23769  dvmptres2  23770  dvmptneg  23774  dvmptsub  23775  dvmptcj  23776  dvmptco  23780  dveflem  23787  dvlip  23801  dvlipcn  23802  dvlip2  23803  dvcvx  23828  dvfsumle  23829  dvfsumabs  23831  dvfsumlem1  23834  dvfsumlem2  23835  ftc2  23852  ftc2ditglem  23853  itgparts  23855  itgsubstlem  23856  itgsubst  23857  fta1glem1  23970  fta1blem  23973  plyeq0lem  24011  plymullem1  24015  coeeulem  24025  coe0  24057  coesub  24058  dvply1  24084  plydivlem4  24096  plyrem  24105  fta1lem  24107  vieta1  24112  plyexmo  24113  elqaalem2  24120  aareccl  24126  aannenlem1  24128  aaliou3lem2  24143  dvtaylp  24169  taylthlem1  24172  radcnvlem1  24212  pserdvlem2  24227  efcvx  24248  ptolemy  24293  tangtx  24302  efif1olem3  24335  efif1olem4  24336  efabl  24341  lognegb  24381  efiarg  24398  cosargd  24399  tanarg  24410  logtayl  24451  cxpneg  24472  cxpsub  24473  cxprec  24477  cxproot  24481  cxpsqrt  24494  cxpcn3lem  24533  cxpaddlelem  24537  abscxpbnd  24539  root1eq1  24541  cxpeq  24543  logrec  24546  isosctrlem2  24594  isosctrlem3  24595  isosctr  24596  ssscongptld  24597  chordthmlem  24604  heron  24610  quad2  24611  dcubic1lem  24615  mcubic  24619  cubic2  24620  cubic  24621  dquartlem2  24624  dquart  24625  quart1lem  24627  quart1  24628  asinlem2  24641  asinlem3  24643  asinsin  24664  sinacos  24677  atanlogsublem  24687  efiatan2  24689  2efiatan  24690  tanatan  24691  atantan  24695  atans2  24703  dvatan  24707  atantayl  24709  atantayl2  24710  log2cnv  24716  rlimcnp2  24738  cxplim  24743  cxp2lim  24748  cvxcl  24756  scvxcvx  24757  zetacvg  24786  lgamgulmlem4  24803  lgamcvg2  24826  gamp1  24829  wilthlem1  24839  wilthlem2  24840  ftalem5  24848  basellem3  24854  basellem5  24856  basellem8  24859  mumullem2  24951  musum  24962  musumsum  24963  muinv  24964  sgmppw  24967  1sgmprm  24969  1sgm2ppw  24970  ppiub  24974  logfac2  24987  chpchtsum  24989  perfectlem1  24999  perfectlem2  25000  dchrn0  25020  dchrfi  25025  dchrabs  25030  dchrptlem1  25034  dchrhash  25041  dchr2sum  25043  sum2dchr  25044  bposlem6  25059  bposlem9  25062  lgsvalmod  25086  lgsdilem  25094  lgsne0  25105  lgssq  25107  lgssq2  25108  lgsqr  25121  lgsdchrval  25124  lgsdchr  25125  gausslemma2dlem6  25142  gausslemma2d  25144  lgseisenlem1  25145  lgseisenlem2  25146  lgseisenlem4  25148  lgsquadlem1  25150  lgsquadlem3  25152  lgsquad3  25157  m1lgs  25158  rplogsumlem1  25218  rplogsumlem2  25219  dchrisumlem2  25224  dchrisum0fno1  25245  rpvmasum2  25246  dchrisum0lem1  25250  dchrisum0lem2  25252  mudivsum  25264  mulog2sumlem1  25268  vmalogdivsum  25273  2vmadivsumlem  25274  logsqvma  25276  selberglem2  25280  selberg2lem  25284  selberg3lem1  25291  selberg4lem1  25294  selberg4  25295  pntrsumo1  25299  selbergr  25302  selberg34r  25305  pntrlog2bndlem3  25313  pntrlog2bndlem4  25314  pntibndlem2  25325  pntlemg  25332  pntlemr  25336  pntlemf  25339  ostthlem1  25361  padicabvcxp  25366  ostth3  25372  tgcgrcomlr  25420  tgifscgr  25448  iscgrglt  25454  tgbtwnconn1lem2  25513  tgbtwnconn1lem3  25514  mirne  25607  miduniq2  25627  krippenlem  25630  ragcgr  25647  cgrg3col4  25779  f1otrg  25796  ttgcontlem1  25810  brbtwn2  25830  axsegconlem10  25851  ax5seglem3  25856  ax5seglem6  25859  axpaschlem  25865  axeuclidlem  25887  axcontlem2  25890  axcontlem7  25895  axcontlem8  25896  cusgrsizeindslem  26403  frgrncvvdeq  27289  numclwwlk7  27378  grpoidinvlem1  27486  grpoideu  27491  grporcan  27500  grpolcan  27512  grpoinvop  27515  ablo4  27532  nvscom  27612  nvmul0or  27633  nvz0  27651  smcnlem  27680  ipidsq  27693  sspz  27718  lno0  27739  lnoadd  27741  lnomul  27743  ipasslem3  27816  dipdi  27826  dipassr  27829  dipsubdi  27832  ubthlem2  27855  hvmul0or  28010  hvadd12  28020  hvadd4  28021  hvmulcom  28028  normneg  28129  pjhthlem1  28378  chj12  28521  spanunsni  28566  5oalem2  28642  3oalem2  28650  hoadd4  28771  homul12  28792  hosubdi  28795  honegsubdi  28797  hosub4  28800  adj2  28921  lnopmul  28954  lnopaddi  28958  lnfnaddi  29030  lnfnmuli  29031  cnlnadjlem6  29059  adjeq0  29078  leopmul  29121  opsqrlem1  29127  opsqrlem6  29132  hstnmoc  29210  strlem1  29237  chirredlem3  29379  fpwrelmapffslem  29635  subeqxfrd  29639  xaddeq0  29646  bcm1n  29682  divnumden2  29692  xmulcand  29757  xreceu  29758  bhmafibid1  29772  2sqmod  29776  xrsmulgzz  29806  xrge0adddir  29820  xrge0adddi  29821  abliso  29824  ogrpaddltrbid  29849  ogrpinvlt  29852  archiabllem1a  29873  archiabllem1  29875  archiabllem2c  29877  slmdvs0  29906  dvrcan5  29921  ornglmullt  29935  orngrmullt  29936  rhmunitinv  29950  mdetpmtr2  30018  madjusmdetlem1  30021  mdetlap  30026  qtophaus  30031  qqhval2lem  30153  esumpad  30245  esummulc1  30271  esumsup  30279  measxun2  30401  measssd  30406  inelcarsg  30501  carsggect  30508  carsgclctunlem2  30509  pmeasmono  30514  oddpwdc  30544  eulerpartlemgs2  30570  eulerpartlemn  30571  totprobd  30616  signstfvn  30774  signstfveq0  30782  ftc2re  30804  itgexpif  30812  breprexpnat  30840  circlemethnat  30847  circlevma  30848  circlemethhgt  30849  hgt750lemf  30859  hgt750lemg  30860  hgt750lemb  30862  tgoldbachgt  30869  bnj1379  31027  bnj1321  31221  subfaclim  31296  cvxsconn  31351  resconn  31354  cvmliftmolem1  31389  cvmliftlem7  31399  cvmliftlem13  31404  cvmlift2lem7  31417  cvmlift3lem5  31431  elmsta  31571  msubff1  31579  mthmpps  31605  bcm1nt  31749  faclim2  31760  funsseq  31792  nolesgn2o  31949  nolesgn2ores  31950  nodenselem5  31963  nolt02o  31970  noprefixmo  31973  clsun  32448  topjoin  32485  bj-bary1lem  33290  finxpreclem4  33361  matunitlindflem1  33535  ptrest  33538  poimirlem4  33543  poimirlem6  33545  poimirlem7  33546  poimirlem9  33548  poimirlem11  33550  poimirlem12  33551  poimirlem26  33565  poimirlem27  33566  itg2addnclem  33591  itg2addnclem3  33593  itgaddnclem2  33599  itgsubnc  33602  iblmulc2nc  33605  itgabsnc  33609  ftc2nc  33624  areacirclem1  33630  areacirclem4  33633  areacirc  33635  cocanfo  33642  ablo4pnp  33809  rngolz  33851  rngorz  33852  zerdivemp1x  33876  crngm4  33932  crngohomfo  33935  lfl0  34670  lfladd  34671  lflmul  34673  eqlkr3  34706  olm11  34832  latm12  34835  cmtcomlemN  34853  omlspjN  34866  hlatj12  34975  1cvrjat  35079  dalemrotyz  35262  padd12N  35443  pmapjlln1  35459  atmod2i1  35465  pmapocjN  35534  pnonsingN  35537  pexmidN  35573  lhp2at0  35636  lhpelim  35641  ltrncnv  35750  ltrnmwOLD  35756  cdleme7c  35850  cdleme15b  35880  cdlemednpq  35904  cdleme20m  35928  cdleme22cN  35947  cdleme22d  35948  cdleme23b  35955  cdleme30a  35983  cdleme35h  36061  cdlemeg46frv  36130  cdlemg2fv2  36205  cdlemg2l  36208  cdlemg2m  36209  cdlemg8c  36234  cdlemg10bALTN  36241  cdlemg12  36255  cdlemg13a  36256  cdlemg18c  36285  cdlemg19  36289  trlcoat  36328  cdlemg47  36341  tendo1ne0  36433  cdlemk9  36444  cdlemk9bN  36445  dia2dimlem1  36670  tendolinv  36711  tendorinv  36712  dvhlveclem  36714  doca3N  36733  dihmeetlem7N  36916  dihjatc1  36917  dihmeetlem18N  36930  dochnoncon  36997  dihjatc  37023  dihjatcclem1  37024  dihjatcclem4  37027  dochsnkr  37078  lcfl7lem  37105  lcfl8  37108  lcfl9a  37111  lclkrlem1  37112  lclkrlem2e  37117  lclkrlem2j  37122  lcfrlem1  37148  lcfrlem9  37156  lcfrlem23  37171  lcfrlem31  37179  mapd0  37271  mapdpglem21  37298  baerlem3lem1  37313  baerlem5alem1  37314  mapdindp4  37329  mapdh6gN  37348  hdmap1l6g  37423  hgmapval0  37501  hgmaprnlem1N  37505  hlhilhillem  37569  diophrw  37639  eldioph2lem1  37640  pellexlem2  37711  pellexlem6  37715  pellex  37716  pell1234qrne0  37734  pell1234qrreccl  37735  pell1qrgaplem  37754  rmxm1  37816  oddcomabszz  37826  jm2.19lem1  37873  jm3.1lem2  37902  dnnumch3  37934  pwssplit4  37976  flcidc  38061  deg1mhm  38102  itgpowd  38117  radcnvrat  38830  nzprmdif  38835  hashnzfz  38836  dvsconst  38846  dvsid  38847  expgrowth  38851  bccm1k  38858  bccn1  38860  binomcxplemnotnn0  38872  subadd4b  39808  uzinico2  40107  sumnnodd  40180  limsupresuz  40253  limsupequzlem  40272  liminfresre  40329  liminfresuz  40334  climliminflimsupd  40351  icccncfext  40418  dvresntr  40450  itgsinexplem1  40487  itgsinexp  40488  stoweidlem1  40536  wallispi2lem2  40607  stirlinglem3  40611  stirlinglem5  40613  stirlinglem10  40618  stirlinglem15  40623  dirkertrigeqlem3  40635  dirkercncflem2  40639  fourierdlem26  40668  fourierdlem42  40684  fourierdlem66  40707  fourierdlem73  40714  fourierdlem81  40722  fourierdlem83  40724  fourierdlem107  40748  etransclem23  40792  meaiininclem  41021  vonvolmbl  41196  iccvonmbllem  41213  sigaradd  41376  cevathlem1  41377  imarnf1pr  41624  m1mod0mod1  41664  fmtnorec3  41785  proththd  41856  perfectALTVlem1  41955  perfectALTVlem2  41956  rnglz  42209  pw2m1lepw2m1  42635  nnpw2pmod  42702  dignn0flhalflem1  42734  aacllem  42875  amgmlemALT  42877  young2d  42879
 Copyright terms: Public domain W3C validator