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

Theorem 3eqtr3d 2492
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 2486 . 2  |-  ( ph  ->  B  =  C )
4 3eqtr3d.3 . 2  |-  ( ph  ->  B  =  D )
53, 4eqtr3d 2486 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1383
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-cleq 2435
This theorem is referenced by:  mpteqb  5955  fvmptt  5956  fsnunfv  6096  f1ocnvfv1  6167  f1ocnvfv2  6168  fcof1  6175  weniso  6235  caov12d  6481  caov13d  6483  caov411d  6485  caovmo  6497  grprinvlem  6498  grprinvd  6499  grpridd  6500  onovuni  7015  tfrlem5  7051  seqomlem1  7117  seqomlem4  7120  onasuc  7180  onesuc  7182  oeeui  7253  fopwdom  7627  unxpdomlem2  7727  cantnfres  8099  cnfcom2lem  8148  cnfcom2  8149  cnfcom2lemOLD  8156  cnfcom2OLD  8157  cardiun  8366  ackbij1lem16  8618  ackbij2lem2  8623  fpwwe2lem6  9016  fpwwe2lem8  9018  canthp1lem2  9034  mul12  9749  mul4  9752  addid1  9763  addcan  9767  addcom  9769  addcomd  9785  add12  9796  ppncan  9866  addsub4  9867  muladd  9995  mulcand  10188  receu  10200  div13  10234  divdivdiv  10251  divcan5  10252  divdiv1  10261  divdiv2  10262  halfaddsub  10778  uzindOLD  10963  xadddi  11496  xov1plusxeqvd  11675  fztp  11745  flzadd  11938  fldiv  11966  addmodid  12015  modnegd  12021  modsub12d  12023  2submod  12027  seqm1  12103  seqcaopr  12123  seqf1o  12127  exprec  12186  expsub  12192  zesq  12268  digit1  12279  discr1  12281  discr  12282  facnn2  12341  faclbnd6  12356  hashfz1  12398  hashdom  12426  hashun  12429  hashbclem  12480  hashfac  12486  seqcoll  12491  wrdlenccats1lenm1  12606  ccatopth  12674  repsw2  12867  repsw3  12868  shftval3  12888  crre  12926  resub  12939  imsub  12947  cjsub  12961  abslem2  13151  sqreulem  13171  climshft2  13384  isercolllem2  13467  iseraltlem2  13484  iseraltlem3  13485  fsumsub  13582  telfsumo  13595  telfsumo2  13596  hashiun  13615  bcxmas  13626  climcndslem1  13640  climcndslem2  13641  trireciplem  13652  geoser  13657  geo2sum2  13662  sinsub  13780  cossub  13781  rpnnen2lem10  13834  ruclem12  13851  divalglem9  13936  bitsinv1lem  13968  bitsinv1  13969  bitsf1  13973  sadasslem  13997  bitsres  14000  smup1  14016  smumul  14020  modgcd  14051  absmulgcd  14062  gcdmultiplez  14066  eucalg  14093  numdensq  14164  dfphi2  14181  phiprm  14184  fermltl  14191  prmdiveq  14193  odzdvds  14199  powm2modprm  14205  modprm0  14207  coprimeprodsq  14210  pythagtriplem6  14222  pythagtriplem7  14223  pythagtriplem12  14227  pythagtriplem16  14231  pcaddlem  14284  sumhash  14292  pcfac  14295  pockthlem  14300  prmreclem6  14316  4sqlem12  14351  4sqlem15  14354  vdwlem3  14378  vdwlem6  14381  vdwlem9  14384  ramub1lem2  14422  cshwshashlem2  14458  qusaddvallem  14825  xpsaddlem  14849  xpsvsca  14853  mrcun  14896  homfeqval  14969  comfeqval  14980  sectcan  15027  sectco  15028  sectmon  15049  monsect  15050  funcsect  15115  setcmon  15288  resscatc  15306  catciso  15308  evlfcllem  15364  curf2cl  15374  curfcl  15375  yonedalem4c  15420  yonedalem3b  15422  yonedainv  15424  latj12  15600  mnd12g  15810  resmhm  15864  pwsco2mhm  15876  frmdup3lem  15908  grprcan  15957  grplcan  15976  grpinv11  15981  grpinvnz  15983  grplmulf1o  15986  grpinvpropd  15987  grpinvadd  15990  grpsubsub4  16005  mulgz  16037  mulgdirlem  16040  mulgdir  16041  mulgass  16046  mulgsubdir  16047  mulgpropd  16049  pwsmulg  16058  imasgrp2  16059  mhmid  16065  mhmmnd  16066  isnsg3  16109  nmzsubg  16116  ssnmz  16117  eqger  16125  eqglact  16126  ghminv  16148  conjnmz  16174  subgga  16212  gasubg  16214  galcan  16216  gacan  16217  cntzsubg  16248  cntzmhm  16250  psgnunilem2  16394  sylow1lem1  16492  sylow2blem2  16515  sylow2blem3  16516  lsmmod  16567  lsmpropd  16569  lsmdisj2  16574  subgdisj1  16583  subgdisj2  16584  efgredleme  16635  efgredlemd  16636  efgredlemc  16637  efgredlem  16639  frgpup3lem  16669  mulgdi  16709  ghmcmn  16714  lsm4  16740  cygabl  16767  gsummhm2  16835  gsummhm2OLD  16836  gsumpt  16862  gsumptOLD  16863  gsum2d  16873  gsum2dOLD  16874  dprdfeq0  16936  dprdfeq0OLD  16943  ablfac1eu  16998  ringcom  17101  isringd  17107  ringlz  17109  ringrz  17110  ring1eq0  17112  ringmneg1  17116  gsumdixpOLD  17131  gsumdixp  17132  unitgrp  17190  irredrmul  17230  drngmul0or  17291  subrginv  17319  subrgunit  17321  abvrec  17359  srngnvl  17379  srngadd  17380  srngmul  17381  issrngd  17384  lmodvs0  17420  lmodvneg1  17427  lmodcom  17430  lmodsubdi  17441  lmodvsinv  17556  lmodvsinv2  17557  lmhmvsca  17565  lvecvs0or  17628  lvecinv  17633  lspsnvs  17634  lspabs2  17640  lspfixed  17648  lspsolv  17663  unitrrg  17816  asclpropd  17869  psrass1lem  17903  psrlidm  17930  psrlidmOLD  17931  psrridm  17932  psrridmOLD  17933  mvrf1  17955  mplmon2mul  18040  evlslem1  18058  evlseu  18059  evlssca  18065  evlsvar  18066  coe1pwmul  18194  pf1ind  18265  prmirredlem  18396  prmirredlemOLD  18399  mulgrhm2  18406  mulgrhm2OLD  18409  chrrhm  18441  znidomb  18473  psgnghm  18489  psgninv  18491  zrhpsgnodpm  18501  evpmodpmf1o  18505  psgndiflemB  18509  ip0r  18545  ipdir  18547  ipdi  18548  ipass  18553  ipassr  18554  phlpropd  18563  ocvpj  18621  uvcresum  18697  lmimlbs  18744  gsumcom3  18774  mat0dimbas0  18841  mdetrlin  18977  mdetrsca  18978  mdetr0  18980  mdetunilem8  18994  mdetuni0  18996  mdetmul  18998  maducoeval2  19015  madurid  19019  madulid  19020  matinv  19052  matunit  19053  slesolinv  19055  slesolinvbi  19056  cpmadugsumlemF  19250  restin  19540  cncmp  19765  cmpsublem  19772  conndisj  19790  cnconn  19796  kgencmp2  19920  ufldom  20336  tgplacthmeo  20475  ghmcnp  20486  qustgpopn  20491  qustgphaus  20494  tsmsxplem2  20529  tususp  20648  xpsdsval  20757  blpnfctr  20812  xmssym  20841  ressxms  20901  isngp2  20990  ngppropd  21024  nminvr  21051  blcvx  21176  icccvx  21323  pcohtpylem  21392  pcohtpy  21393  cvsmuleqdivd  21484  cvsdiveqd  21485  pjthlem1  21725  ovollb2lem  21772  ovolicc2lem1  21801  ovolicc2lem5  21805  volsup  21839  ovolioo  21851  uniiccdif  21860  uniioombllem3  21867  uniioombllem4  21868  vitalilem3  21892  itg1sub  21989  itg2const  22020  iblcnlem1  22067  itgcnlem  22069  itgaddlem2  22103  itgsub  22105  itgabs  22114  ditgsplit  22138  dvmulbr  22215  dvcmul  22220  dvcmulf  22221  dvrec  22231  dvmptres3  22232  dvmptadd  22236  dvmptmul  22237  dvmptres2  22238  dvmptneg  22242  dvmptsub  22243  dvmptcj  22244  dvmptco  22248  dveflem  22253  dvlip  22267  dvlipcn  22268  dvlip2  22269  dvcvx  22294  dvfsumle  22295  dvfsumabs  22297  dvfsumlem1  22300  dvfsumlem2  22301  ftc2  22318  ftc2ditglem  22319  itgparts  22321  itgsubstlem  22322  itgsubst  22323  fta1glem1  22439  fta1blem  22442  plyeq0lem  22480  plymullem1  22484  coeeulem  22494  coe0  22525  coesub  22526  dvply1  22552  plydivlem4  22564  plyrem  22573  fta1lem  22575  vieta1  22580  plyexmo  22581  elqaalem2  22588  aareccl  22594  aannenlem1  22596  aaliou3lem2  22611  dvtaylp  22637  taylthlem1  22640  radcnvlem1  22680  pserdvlem2  22695  efcvx  22716  ptolemy  22761  tangtx  22770  efif1olem3  22803  efif1olem4  22804  efabl  22809  lognegb  22846  efiarg  22864  cosargd  22865  tanarg  22876  logtayl  22913  cxpneg  22934  cxpsub  22935  cxprec  22939  cxproot  22943  cxpsqrt  22956  cxpcn3lem  22993  cxpaddlelem  22997  abscxpbnd  22999  root1eq1  23001  cxpeq  23003  logrec  23023  isosctrlem2  23025  isosctrlem3  23026  isosctr  23027  ssscongptld  23028  chordthmlem  23035  heron  23041  quad2  23042  dcubic1lem  23046  mcubic  23050  cubic2  23051  cubic  23052  dquartlem2  23055  dquart  23056  quart1lem  23058  quart1  23059  asinlem2  23072  asinlem3  23074  asinsin  23095  sinacos  23108  atanlogsublem  23118  efiatan2  23120  2efiatan  23121  tanatan  23122  atantan  23126  atans2  23134  dvatan  23138  atantayl  23140  atantayl2  23141  log2cnv  23147  rlimcnp2  23168  cxplim  23173  cxp2lim  23178  cvxcl  23186  scvxcvx  23187  wilthlem1  23214  wilthlem2  23215  ftalem5  23222  basellem3  23228  basellem5  23230  basellem8  23233  mumullem2  23326  musum  23339  musumsum  23340  muinv  23341  sgmppw  23344  1sgmprm  23346  1sgm2ppw  23347  ppiub  23351  logfac2  23364  chpchtsum  23366  perfectlem1  23376  perfectlem2  23377  dchrn0  23397  dchrfi  23402  dchrabs  23407  dchrptlem1  23411  dchrhash  23418  dchr2sum  23420  sum2dchr  23421  bposlem6  23436  bposlem9  23439  lgsvalmod  23462  lgsdilem  23469  lgsne0  23480  lgssq  23482  lgssq2  23483  lgsqr  23493  lgsdchrval  23494  lgsdchr  23495  lgseisenlem1  23496  lgseisenlem2  23497  lgseisenlem4  23499  lgsquadlem1  23501  lgsquadlem3  23503  lgsquad3  23508  m1lgs  23509  rplogsumlem1  23541  rplogsumlem2  23542  dchrisumlem2  23547  dchrisum0fno1  23568  rpvmasum2  23569  dchrisum0lem1  23573  dchrisum0lem2  23575  mudivsum  23587  mulog2sumlem1  23591  vmalogdivsum  23596  2vmadivsumlem  23597  logsqvma  23599  selberglem2  23603  selberg2lem  23607  selberg3lem1  23614  selberg4lem1  23617  selberg4  23618  pntrsumo1  23622  selbergr  23625  selberg34r  23628  pntrlog2bndlem3  23636  pntrlog2bndlem4  23637  pntibndlem2  23648  pntlemg  23655  pntlemr  23659  pntlemf  23662  ostthlem1  23684  padicabvcxp  23689  ostth3  23695  tgcgrcomlr  23743  tgifscgr  23772  tgbtwnconn1lem2  23832  tgbtwnconn1lem3  23833  miduniq2  23936  krippenlem  23939  ragcgr  23956  f1otrg  24046  ttgcontlem1  24060  brbtwn2  24080  axsegconlem10  24101  ax5seglem3  24106  ax5seglem6  24109  axpaschlem  24115  axeuclidlem  24137  axcontlem2  24140  axcontlem7  24145  axcontlem8  24146  cusgrasizeindslem3  24347  frgrancvvdeq  24914  frgrancvvdgeq  24915  numclwwlk7  24986  grpoidinvlem1  25078  grpoideu  25083  grporcan  25095  grpolcan  25107  grpoasscan1  25111  grpoinvop  25115  grpopnpcan2  25127  gxsuc  25146  gxsub  25150  gxmul  25152  ablo4  25161  subgoinv  25182  ablomul  25229  ghgrpOLD  25242  ghabloOLD  25243  rngolz  25275  rngorz  25276  zerdivemp1  25308  nvadd12  25388  nvscom  25396  nvmul0or  25419  nvz0  25443  smcnlem  25479  ipidsq  25495  sspz  25520  lno0  25543  lnoadd  25545  lnomul  25547  ipasslem3  25620  dipdi  25630  dipassr  25633  dipsubdi  25636  ubthlem2  25659  hvmul0or  25814  hvadd12  25824  hvadd4  25825  hvmulcom  25832  normneg  25933  pjhthlem1  26181  chj12  26324  spanunsni  26369  5oalem2  26445  3oalem2  26453  mayete3iOLD  26519  hoadd4  26575  homul12  26596  hosubdi  26599  honegsubdi  26601  hosub4  26604  adj2  26725  lnopmul  26758  lnopaddi  26762  lnfnaddi  26834  lnfnmuli  26835  cnlnadjlem6  26863  adjeq0  26882  leopmul  26925  opsqrlem1  26931  opsqrlem6  26936  hstnmoc  27014  strlem1  27041  chirredlem3  27183  fpwrelmapffslem  27427  subeqxfrd  27431  addeqxfrd  27432  xaddeq0  27445  bcm1n  27472  divnumden2  27481  xmulcand  27490  xreceu  27491  bhmafibid1  27505  2sqmod  27509  xrsmulgzz  27539  xrge0adddir  27555  xrge0adddi  27556  abliso  27559  ogrpaddltrbid  27584  ogrpinvlt  27587  archiabllem1a  27608  archiabllem1  27610  archiabllem2c  27612  slmdvs0  27641  dvrcan5  27656  ornglmullt  27670  orngrmullt  27671  rhmunitinv  27685  qtophaus  27712  qqhval2lem  27835  esummulc1  27960  measxun2  28054  measssd  28059  oddpwdc  28166  eulerpartlemgs2  28192  eulerpartlemn  28193  totprobd  28238  signstfvn  28399  signstfveq0  28407  zetacvg  28430  lgamgulmlem4  28447  lgamcvg2  28470  gamp1  28473  subfaclim  28505  cvxscon  28561  rescon  28564  cvmliftmolem1  28599  cvmliftlem7  28609  cvmliftlem13  28614  cvmlift2lem7  28627  cvmlift3lem5  28641  elmsta  28781  msubff1  28789  mthmpps  28815  ghomf1olem  28907  fprodm1  29071  fallfacfwd  29133  binomfallfaclem2  29137  faclim2  29148  funsseq  29174  bpolydiflem  29791  bpoly4  29796  fsumcube  29797  ptrest  30023  itg2addnclem  30041  itg2addnclem3  30043  itgaddnclem2  30049  itgsubnc  30052  iblmulc2nc  30055  itgabsnc  30059  ftc2nc  30074  areacirclem1  30082  areacirclem4  30085  areacirc  30087  clsun  30121  topjoin  30158  cocanfo  30183  ablo4pnp  30317  zerdivemp1x  30333  crngm4  30375  crngohomfo  30378  diophrw  30667  eldioph2lem1  30668  pellexlem2  30741  pellexlem6  30745  pellex  30746  pell1234qrne0  30764  pell1234qrreccl  30765  pell1qrgaplem  30784  rmxm1  30845  oddcomabszz  30855  jm2.19lem1  30906  jm3.1lem2  30935  dnnumch3  30968  pwssplit4  31010  flcidc  31099  hashgcdlem  31133  deg1mhm  31143  itgpowd  31158  radcnvrat  31171  lcmgcd  31189  lcmid  31191  nzprmdif  31200  hashnzfz  31201  dvsconst  31211  dvsid  31212  expgrowth  31216  subadd4b  31413  sumnnodd  31544  icccncfext  31597  dvresntr  31617  itgsinexplem1  31642  itgsinexp  31643  stoweidlem1  31672  wallispi2lem2  31743  stirlinglem3  31747  stirlinglem5  31749  stirlinglem10  31754  stirlinglem15  31759  dirkertrigeqlem3  31771  dirkercncflem2  31775  fourierdlem26  31804  fourierdlem42  31820  fourierdlem66  31844  fourierdlem73  31851  fourierdlem81  31859  fourierdlem83  31861  fourierdlem107  31885  sigaradd  31921  cevathlem1  31922  imarnf1pr  32147  usgrauvtxvd  32196  bnj1379  33622  bnj1321  33816  bj-bary1lem  34419  fsumshftdOLD  34423  lfl0  34530  lfladd  34531  lflmul  34533  eqlkr3  34566  olm11  34692  latm12  34695  cmtcomlemN  34713  omlspjN  34726  hlatj12  34835  1cvrjat  34939  dalemrotyz  35122  padd12N  35303  pmapjlln1  35319  atmod2i1  35325  pmapocjN  35394  pnonsingN  35397  pexmidN  35433  lhp2at0  35496  lhpelim  35501  ltrncnv  35610  ltrnmwOLD  35616  cdleme7c  35710  cdleme15b  35740  cdlemednpq  35764  cdleme20yOLD  35768  cdleme20m  35789  cdleme22cN  35808  cdleme22d  35809  cdleme23b  35816  cdleme30a  35844  cdleme35h  35922  cdlemeg46frv  35991  cdlemg2fv2  36066  cdlemg2l  36069  cdlemg2m  36070  cdlemg8c  36095  cdlemg10bALTN  36102  cdlemg12  36116  cdlemg13a  36117  cdlemg18c  36146  cdlemg19  36150  trlcoat  36189  cdlemg47  36202  tendo1ne0  36294  cdlemk9  36305  cdlemk9bN  36306  dia2dimlem1  36531  tendolinv  36572  tendorinv  36573  dvhlveclem  36575  doca3N  36594  dihmeetlem7N  36777  dihjatc1  36778  dihmeetlem18N  36791  dochnoncon  36858  dihjatc  36884  dihjatcclem1  36885  dihjatcclem4  36888  dochsnkr  36939  lcfl7lem  36966  lcfl8  36969  lcfl9a  36972  lclkrlem1  36973  lclkrlem2e  36978  lclkrlem2j  36983  lcfrlem1  37009  lcfrlem9  37017  lcfrlem23  37032  lcfrlem31  37040  mapd0  37132  mapdpglem21  37159  baerlem3lem1  37174  baerlem5alem1  37175  mapdindp4  37190  mapdh6gN  37209  hdmap1l6g  37284  hgmapval0  37362  hgmaprnlem1N  37366  hlhilhillem  37430
  Copyright terms: Public domain W3C validator