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

Theorem 3eqtr3d 2431
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 2425 . 2  |-  ( ph  ->  B  =  C )
4 3eqtr3d.3 . 2  |-  ( ph  ->  B  =  D )
53, 4eqtr3d 2425 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1399
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-cleq 2374
This theorem is referenced by:  mpteqb  5872  fvmptt  5873  fsnunfv  6013  f1ocnvfv1  6083  f1ocnvfv2  6084  fcof1  6091  weniso  6151  caov12d  6395  caov13d  6397  caov411d  6399  caovmo  6411  grprinvlem  6412  grprinvd  6413  grpridd  6414  onovuni  6931  tfrlem5  6967  seqomlem1  7033  seqomlem4  7036  onasuc  7096  onesuc  7098  oeeui  7169  fopwdom  7544  unxpdomlem2  7641  cantnfres  8009  cnfcom2lem  8058  cnfcom2  8059  cnfcom2lemOLD  8066  cnfcom2OLD  8067  cardiun  8276  ackbij1lem16  8528  ackbij2lem2  8533  fpwwe2lem6  8924  fpwwe2lem8  8926  canthp1lem2  8942  mul12  9657  mul4  9660  addid1  9671  addcan  9675  addcom  9677  addcomd  9693  add12  9704  ppncan  9774  addsub4  9775  muladd  9907  mulcand  10099  receu  10111  div13  10145  divdivdiv  10162  divcan5  10163  divdiv1  10172  divdiv2  10173  halfaddsub  10689  xadddi  11408  xov1plusxeqvd  11587  fztp  11658  flzadd  11859  fldiv  11887  modnegd  11945  modsub12d  11947  2submod  11951  seqm1  12027  seqcaopr  12047  seqf1o  12051  exprec  12110  expsub  12116  zesq  12191  digit1  12202  discr1  12204  discr  12205  facnn2  12264  faclbnd6  12279  hashfz1  12321  hashdom  12350  hashun  12353  hashbclem  12405  hashfac  12411  seqcoll  12416  ccatopth  12606  repsw2  12799  repsw3  12800  shftval3  12911  crre  12949  resub  12962  imsub  12970  cjsub  12984  abslem2  13174  sqreulem  13194  climshft2  13407  isercolllem2  13490  iseraltlem2  13507  iseraltlem3  13508  fsumsub  13605  telfsumo  13618  telfsumo2  13619  hashiun  13638  bcxmas  13649  climcndslem1  13663  climcndslem2  13664  trireciplem  13675  geoser  13680  geo2sum2  13685  fprodm1  13773  sinsub  13905  cossub  13906  rpnnen2lem10  13959  ruclem12  13976  divalglem9  14061  bitsinv1lem  14093  bitsinv1  14094  bitsf1  14098  sadasslem  14122  bitsres  14125  smup1  14141  smumul  14145  modgcd  14176  absmulgcd  14187  gcdmultiplez  14191  eucalg  14218  numdensq  14289  dfphi2  14306  phiprm  14309  fermltl  14316  prmdiveq  14318  odzdvds  14324  powm2modprm  14330  modprm0  14332  coprimeprodsq  14335  pythagtriplem6  14347  pythagtriplem7  14348  pythagtriplem12  14352  pythagtriplem16  14356  pcaddlem  14409  sumhash  14417  pcfac  14420  pockthlem  14425  prmreclem6  14441  4sqlem12  14476  4sqlem15  14479  vdwlem3  14503  vdwlem6  14506  vdwlem9  14509  ramub1lem2  14547  cshwshashlem2  14583  qusaddvallem  14958  xpsaddlem  14982  xpsvsca  14986  mrcun  15029  homfeqval  15103  comfeqval  15114  sectcan  15161  sectco  15162  sectmon  15188  monsect  15189  funcsect  15278  setcmon  15483  resscatc  15501  catciso  15503  evlfcllem  15607  curf2cl  15617  curfcl  15618  yonedalem4c  15663  yonedalem3b  15665  yonedainv  15667  latj12  15843  mnd12g  16053  resmhm  16107  pwsco2mhm  16119  frmdup3lem  16151  grprcan  16200  grplcan  16219  grpinv11  16224  grpinvnz  16226  grplmulf1o  16229  grpinvpropd  16230  grpinvadd  16233  grpsubsub4  16248  mulgz  16280  mulgdirlem  16283  mulgdir  16284  mulgass  16289  mulgsubdir  16290  mulgpropd  16292  pwsmulg  16301  imasgrp2  16302  mhmid  16308  mhmmnd  16309  isnsg3  16352  nmzsubg  16359  ssnmz  16360  eqger  16368  eqglact  16369  ghminv  16391  conjnmz  16417  subgga  16455  gasubg  16457  galcan  16459  gacan  16460  cntzsubg  16491  cntzmhm  16493  psgnunilem2  16637  sylow1lem1  16735  sylow2blem2  16758  sylow2blem3  16759  lsmmod  16810  lsmpropd  16812  lsmdisj2  16817  subgdisj1  16826  subgdisj2  16827  efgredleme  16878  efgredlemd  16879  efgredlemc  16880  efgredlem  16882  frgpup3lem  16912  mulgdi  16952  ghmcmn  16957  lsm4  16983  cygabl  17010  gsummhm2  17077  gsummhm2OLD  17078  gsumpt  17102  gsumptOLD  17103  gsum2d  17113  gsum2dOLD  17114  dprdfeq0  17175  dprdfeq0OLD  17182  ablfac1eu  17237  ringcom  17340  isringd  17346  ringlz  17348  ringrz  17349  ring1eq0  17351  ringmneg1  17355  gsumdixpOLD  17370  gsumdixp  17371  unitgrp  17429  irredrmul  17469  drngmul0or  17530  subrginv  17558  subrgunit  17560  abvrec  17598  srngnvl  17618  srngadd  17619  srngmul  17620  issrngd  17623  lmodvs0  17659  lmodvneg1  17666  lmodcom  17669  lmodsubdi  17680  lmodvsinv  17795  lmodvsinv2  17796  lmhmvsca  17804  lvecvs0or  17867  lvecinv  17872  lspsnvs  17873  lspabs2  17879  lspfixed  17887  lspsolv  17902  unitrrg  18055  asclpropd  18108  psrass1lem  18142  psrlidm  18169  psrlidmOLD  18170  psrridm  18171  psrridmOLD  18172  mvrf1  18194  mplmon2mul  18279  evlslem1  18297  evlseu  18298  evlssca  18304  evlsvar  18305  coe1pwmul  18433  pf1ind  18504  prmirredlem  18623  mulgrhm2  18629  chrrhm  18661  znidomb  18691  psgnghm  18707  psgninv  18709  zrhpsgnodpm  18719  evpmodpmf1o  18723  psgndiflemB  18727  ip0r  18763  ipdir  18765  ipdi  18766  ipass  18771  ipassr  18772  phlpropd  18781  ocvpj  18839  uvcresum  18913  lmimlbs  18956  gsumcom3  18986  mat0dimbas0  19053  mdetrlin  19189  mdetrsca  19190  mdetr0  19192  mdetunilem8  19206  mdetuni0  19208  mdetmul  19210  maducoeval2  19227  madurid  19231  madulid  19232  matinv  19264  matunit  19265  slesolinv  19267  slesolinvbi  19268  cpmadugsumlemF  19462  restin  19753  cncmp  19978  cmpsublem  19985  conndisj  20002  cnconn  20008  kgencmp2  20132  ufldom  20548  tgplacthmeo  20687  ghmcnp  20698  qustgpopn  20703  qustgphaus  20706  tsmsxplem2  20741  tususp  20860  xpsdsval  20969  blpnfctr  21024  xmssym  21053  ressxms  21113  isngp2  21202  ngppropd  21236  nminvr  21263  blcvx  21388  icccvx  21535  pcohtpylem  21604  pcohtpy  21605  cvsmuleqdivd  21696  cvsdiveqd  21697  pjthlem1  21937  ovollb2lem  21984  ovolicc2lem1  22013  ovolicc2lem5  22017  volsup  22051  ovolioo  22063  uniiccdif  22072  uniioombllem3  22079  uniioombllem4  22080  vitalilem3  22104  itg1sub  22201  itg2const  22232  iblcnlem1  22279  itgcnlem  22281  itgaddlem2  22315  itgsub  22317  itgabs  22326  ditgsplit  22350  dvmulbr  22427  dvcmul  22432  dvcmulf  22433  dvrec  22443  dvmptres3  22444  dvmptadd  22448  dvmptmul  22449  dvmptres2  22450  dvmptneg  22454  dvmptsub  22455  dvmptcj  22456  dvmptco  22460  dveflem  22465  dvlip  22479  dvlipcn  22480  dvlip2  22481  dvcvx  22506  dvfsumle  22507  dvfsumabs  22509  dvfsumlem1  22512  dvfsumlem2  22513  ftc2  22530  ftc2ditglem  22531  itgparts  22533  itgsubstlem  22534  itgsubst  22535  fta1glem1  22651  fta1blem  22654  plyeq0lem  22692  plymullem1  22696  coeeulem  22706  coe0  22738  coesub  22739  dvply1  22765  plydivlem4  22777  plyrem  22786  fta1lem  22788  vieta1  22793  plyexmo  22794  elqaalem2  22801  aareccl  22807  aannenlem1  22809  aaliou3lem2  22824  dvtaylp  22850  taylthlem1  22853  radcnvlem1  22893  pserdvlem2  22908  efcvx  22929  ptolemy  22974  tangtx  22983  efif1olem3  23016  efif1olem4  23017  efabl  23022  lognegb  23062  efiarg  23079  cosargd  23080  tanarg  23091  logtayl  23128  cxpneg  23149  cxpsub  23150  cxprec  23154  cxproot  23158  cxpsqrt  23171  cxpcn3lem  23208  cxpaddlelem  23212  abscxpbnd  23214  root1eq1  23216  cxpeq  23218  logrec  23221  isosctrlem2  23269  isosctrlem3  23270  isosctr  23271  ssscongptld  23272  chordthmlem  23279  heron  23285  quad2  23286  dcubic1lem  23290  mcubic  23294  cubic2  23295  cubic  23296  dquartlem2  23299  dquart  23300  quart1lem  23302  quart1  23303  asinlem2  23316  asinlem3  23318  asinsin  23339  sinacos  23352  atanlogsublem  23362  efiatan2  23364  2efiatan  23365  tanatan  23366  atantan  23370  atans2  23378  dvatan  23382  atantayl  23384  atantayl2  23385  log2cnv  23391  rlimcnp2  23413  cxplim  23418  cxp2lim  23423  cvxcl  23431  scvxcvx  23432  wilthlem1  23459  wilthlem2  23460  ftalem5  23467  basellem3  23473  basellem5  23475  basellem8  23478  mumullem2  23571  musum  23584  musumsum  23585  muinv  23586  sgmppw  23589  1sgmprm  23591  1sgm2ppw  23592  ppiub  23596  logfac2  23609  chpchtsum  23611  perfectlem1  23621  perfectlem2  23622  dchrn0  23642  dchrfi  23647  dchrabs  23652  dchrptlem1  23656  dchrhash  23663  dchr2sum  23665  sum2dchr  23666  bposlem6  23681  bposlem9  23684  lgsvalmod  23707  lgsdilem  23714  lgsne0  23725  lgssq  23727  lgssq2  23728  lgsqr  23738  lgsdchrval  23739  lgsdchr  23740  lgseisenlem1  23741  lgseisenlem2  23742  lgseisenlem4  23744  lgsquadlem1  23746  lgsquadlem3  23748  lgsquad3  23753  m1lgs  23754  rplogsumlem1  23786  rplogsumlem2  23787  dchrisumlem2  23792  dchrisum0fno1  23813  rpvmasum2  23814  dchrisum0lem1  23818  dchrisum0lem2  23820  mudivsum  23832  mulog2sumlem1  23836  vmalogdivsum  23841  2vmadivsumlem  23842  logsqvma  23844  selberglem2  23848  selberg2lem  23852  selberg3lem1  23859  selberg4lem1  23862  selberg4  23863  pntrsumo1  23867  selbergr  23870  selberg34r  23873  pntrlog2bndlem3  23881  pntrlog2bndlem4  23882  pntibndlem2  23893  pntlemg  23900  pntlemr  23904  pntlemf  23907  ostthlem1  23929  padicabvcxp  23934  ostth3  23940  tgcgrcomlr  23991  tgifscgr  24020  tgbtwnconn1lem2  24080  tgbtwnconn1lem3  24081  miduniq2  24184  krippenlem  24187  ragcgr  24204  f1otrg  24295  ttgcontlem1  24309  brbtwn2  24329  axsegconlem10  24350  ax5seglem3  24355  ax5seglem6  24358  axpaschlem  24364  axeuclidlem  24386  axcontlem2  24389  axcontlem7  24394  axcontlem8  24395  cusgrasizeindslem3  24596  frgrancvvdeq  25163  frgrancvvdgeq  25164  numclwwlk7  25235  grpoidinvlem1  25323  grpoideu  25328  grporcan  25340  grpolcan  25352  grpoasscan1  25356  grpoinvop  25360  grpopnpcan2  25372  gxsuc  25391  gxsub  25395  gxmul  25397  ablo4  25406  subgoinv  25427  ablomul  25474  ghgrpOLD  25487  ghabloOLD  25488  rngolz  25520  rngorz  25521  zerdivemp1  25553  nvadd12  25633  nvscom  25641  nvmul0or  25664  nvz0  25688  smcnlem  25724  ipidsq  25740  sspz  25765  lno0  25788  lnoadd  25790  lnomul  25792  ipasslem3  25865  dipdi  25875  dipassr  25878  dipsubdi  25881  ubthlem2  25904  hvmul0or  26059  hvadd12  26069  hvadd4  26070  hvmulcom  26077  normneg  26178  pjhthlem1  26426  chj12  26569  spanunsni  26614  5oalem2  26690  3oalem2  26698  hoadd4  26819  homul12  26840  hosubdi  26843  honegsubdi  26845  hosub4  26848  adj2  26969  lnopmul  27002  lnopaddi  27006  lnfnaddi  27078  lnfnmuli  27079  cnlnadjlem6  27107  adjeq0  27126  leopmul  27169  opsqrlem1  27175  opsqrlem6  27180  hstnmoc  27258  strlem1  27285  chirredlem3  27427  fpwrelmapffslem  27705  subeqxfrd  27709  addeqxfrd  27710  xaddeq0  27723  bcm1n  27753  divnumden2  27762  xmulcand  27770  xreceu  27771  bhmafibid1  27785  2sqmod  27789  xrsmulgzz  27819  xrge0adddir  27835  xrge0adddi  27836  abliso  27839  ogrpaddltrbid  27864  ogrpinvlt  27867  archiabllem1a  27888  archiabllem1  27890  archiabllem2c  27892  slmdvs0  27921  dvrcan5  27937  ornglmullt  27951  orngrmullt  27952  rhmunitinv  27966  qtophaus  27993  qqhval2lem  28115  esumpad  28203  esummulc1  28229  esumsup  28237  measxun2  28337  measssd  28342  inelcarsg  28438  carsggect  28445  carsgclctunlem2  28446  oddpwdc  28476  eulerpartlemgs2  28502  eulerpartlemn  28503  totprobd  28548  signstfvn  28709  signstfveq0  28717  zetacvg  28746  lgamgulmlem4  28763  lgamcvg2  28786  gamp1  28789  subfaclim  28821  cvxscon  28877  rescon  28880  cvmliftmolem1  28915  cvmliftlem7  28925  cvmliftlem13  28930  cvmlift2lem7  28943  cvmlift3lem5  28957  elmsta  29097  msubff1  29105  mthmpps  29131  ghomf1olem  29223  fallfacfwd  29324  binomfallfaclem2  29328  faclim2  29339  funsseq  29364  bpolydiflem  29969  bpoly4  29974  fsumcube  29975  ptrest  30213  itg2addnclem  30232  itg2addnclem3  30234  itgaddnclem2  30240  itgsubnc  30243  iblmulc2nc  30246  itgabsnc  30250  ftc2nc  30265  areacirclem1  30273  areacirclem4  30276  areacirc  30278  clsun  30312  topjoin  30349  cocanfo  30374  ablo4pnp  30508  zerdivemp1x  30524  crngm4  30566  crngohomfo  30569  diophrw  30857  eldioph2lem1  30858  pellexlem2  30931  pellexlem6  30935  pellex  30936  pell1234qrne0  30954  pell1234qrreccl  30955  pell1qrgaplem  30974  rmxm1  31035  oddcomabszz  31045  jm2.19lem1  31097  jm3.1lem2  31126  dnnumch3  31159  pwssplit4  31201  flcidc  31291  hashgcdlem  31325  deg1mhm  31335  itgpowd  31350  radcnvrat  31363  lcmgcd  31381  lcmid  31383  nzprmdif  31392  hashnzfz  31393  dvsconst  31403  dvsid  31404  expgrowth  31408  bccm1k  31415  bccn1  31417  binomcxplemnotnn0  31429  subadd4b  31631  sumnnodd  31802  icccncfext  31856  dvresntr  31879  itgsinexplem1  31918  itgsinexp  31919  stoweidlem1  31949  wallispi2lem2  32020  stirlinglem3  32024  stirlinglem5  32026  stirlinglem10  32031  stirlinglem15  32036  dirkertrigeqlem3  32048  dirkercncflem2  32052  fourierdlem26  32081  fourierdlem42  32097  fourierdlem66  32121  fourierdlem73  32128  fourierdlem81  32136  fourierdlem83  32138  fourierdlem107  32162  etransclem23  32206  sigaradd  32249  cevathlem1  32250  m1mod0mod1  32460  mod2eq1n2dvds  32462  perfectALTVlem1  32543  perfectALTVlem2  32544  proththd  32548  imarnf1pr  32630  usgrauvtxvd  32676  rnglz  32890  pw2m1lepw2m1  33327  nnpw2pmod  33404  dignn0flhalflem1  33436  aacllem  33550  bnj1379  34236  bnj1321  34430  bj-bary1lem  35023  fsumshftdOLD  35096  lfl0  35203  lfladd  35204  lflmul  35206  eqlkr3  35239  olm11  35365  latm12  35368  cmtcomlemN  35386  omlspjN  35399  hlatj12  35508  1cvrjat  35612  dalemrotyz  35795  padd12N  35976  pmapjlln1  35992  atmod2i1  35998  pmapocjN  36067  pnonsingN  36070  pexmidN  36106  lhp2at0  36169  lhpelim  36174  ltrncnv  36283  ltrnmwOLD  36289  cdleme7c  36383  cdleme15b  36413  cdlemednpq  36437  cdleme20yOLD  36441  cdleme20m  36462  cdleme22cN  36481  cdleme22d  36482  cdleme23b  36489  cdleme30a  36517  cdleme35h  36595  cdlemeg46frv  36664  cdlemg2fv2  36739  cdlemg2l  36742  cdlemg2m  36743  cdlemg8c  36768  cdlemg10bALTN  36775  cdlemg12  36789  cdlemg13a  36790  cdlemg18c  36819  cdlemg19  36823  trlcoat  36862  cdlemg47  36875  tendo1ne0  36967  cdlemk9  36978  cdlemk9bN  36979  dia2dimlem1  37204  tendolinv  37245  tendorinv  37246  dvhlveclem  37248  doca3N  37267  dihmeetlem7N  37450  dihjatc1  37451  dihmeetlem18N  37464  dochnoncon  37531  dihjatc  37557  dihjatcclem1  37558  dihjatcclem4  37561  dochsnkr  37612  lcfl7lem  37639  lcfl8  37642  lcfl9a  37645  lclkrlem1  37646  lclkrlem2e  37651  lclkrlem2j  37656  lcfrlem1  37682  lcfrlem9  37690  lcfrlem23  37705  lcfrlem31  37713  mapd0  37805  mapdpglem21  37832  baerlem3lem1  37847  baerlem5alem1  37848  mapdindp4  37863  mapdh6gN  37882  hdmap1l6g  37957  hgmapval0  38035  hgmaprnlem1N  38039  hlhilhillem  38103
  Copyright terms: Public domain W3C validator