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

Theorem 3eqtri 2415
Description: An inference from three chained equalities. (Contributed by NM, 29-Aug-1993.)
Hypotheses
Ref Expression
3eqtri.1  |-  A  =  B
3eqtri.2  |-  B  =  C
3eqtri.3  |-  C  =  D
Assertion
Ref Expression
3eqtri  |-  A  =  D

Proof of Theorem 3eqtri
StepHypRef Expression
1 3eqtri.1 . 2  |-  A  =  B
2 3eqtri.2 . . 3  |-  B  =  C
3 3eqtri.3 . . 3  |-  C  =  D
42, 3eqtri 2411 . 2  |-  B  =  D
51, 4eqtri 2411 1  |-  A  =  D
Colors of variables: wff setvar class
Syntax hints:    = 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:  csbid  3356  un23  3577  in32  3624  unvdif  3818  undif2  3820  undifabs  3821  difun2  3823  difdifdir  3831  dfif4  3872  dfif5  3873  tpidm23  4047  dfopif  4128  unisn  4178  dfiunv2  4279  symdif0  4320  symdifid  4322  unidif0  4538  uniop  4664  suc0  4866  unisuc  4868  iunsuc  4874  xpun  4971  dfrn2  5104  dfdmf  5109  dfrnf  5154  res0  5190  resres  5198  xpssres  5220  dfima2  5251  imai  5261  ima0  5264  imaundir  5329  xpima  5359  dmresv  5374  rescnvcnv  5378  dmtpop  5392  rnsnopg  5395  resdmres  5406  dmmpt  5410  dmco  5423  co01  5430  fresaun  5664  dffv4  5771  fvssunirn  5797  fpr  5981  fvsnun2  6009  mpt20  6266  dmoprab  6282  rnoprab  6284  elrnmpt2res  6315  ov6g  6339  1st0  6705  2nd0  6706  dfmpt2  6789  curry1  6791  curry2  6794  fpar  6803  algrflem  6808  dftpos2  6890  tposoprab  6909  tposmpt2  6910  fvmpt2curryd  6918  tfrlem8  6971  seqomlem3  7035  df2o3  7061  omxpenlem  7537  dfsdom2  7559  marypha2lem2  7811  dfsup2OLD  7818  mapfienOLD  8051  scottexs  8218  scott0s  8219  infxpenc2  8312  infxpenc2OLD  8316  kmlem3  8445  cdaassen  8475  ackbij1lem2  8514  compsscnv  8664  fin1a2lem12  8704  mulerpqlem  9244  1lt2nq  9262  axi2m1  9447  2p2e4  10570  numsuc  10907  numsucc  10921  xnegmnf  11330  pnfaddmnf  11350  fz0tp  11699  fzo0to2pr  11798  fzo0to3tp  11799  fzo0to42pr  11800  i4  12173  crreczi  12193  fac1  12259  fac3  12262  hashkf  12309  hashinf  12312  dmhashres  12316  hashun3  12355  cshwsexa  12703  dmtrclfv  12856  abs0  13120  absi  13121  trirecip  13676  geoihalfsum  13693  esum  13818  tan0  13888  coshval  13892  ef01bndlem  13921  3dvds  14052  sadc0  14106  gcdmodi  14562  karatsuba  14572  43prm  14609  139prm  14611  631prm  14614  1259lem1  14615  1259lem2  14616  1259lem3  14617  1259lem4  14618  1259lem5  14619  2503lem1  14621  2503lem2  14622  2503lem3  14623  4001lem2  14626  4001lem3  14627  4001lem4  14628  4001prm  14629  ndxarg  14654  xpsc  14964  pmtrsn  16661  psgnprfval1  16664  sylow2a  16756  0frgp  16914  gsumval3OLD  17025  gsumzaddlemOLD  17053  ablfac1eu  17237  sralem  17936  opsrtoslem2  18262  ply1plusgfvi  18396  pf1rcl  18498  restcld  19759  neitr  19767  txbasval  20192  txindis  20220  cnmpt1st  20254  cnmpt2nd  20255  ufildr  20517  restmetu  21175  reust  21898  ismbl  22022  mbfimaopnlem  22147  itg10  22180  itg2cnlem2  22254  itgz  22272  dvmptid  22445  cos2pi  22954  tan4thpi  22992  sincos6thpi  22993  pige3  22995  dfrelog  23038  logm1  23061  dvlog  23119  efopnlem2  23125  cxpexp  23136  root1id  23215  ang180lem2  23260  1cubrlem  23288  quart1  23303  atandm2  23324  efiasin  23335  asinsinlem  23338  asinsin  23339  asin1  23341  acos1  23342  atancj  23357  atanlogsublem  23362  efiatan2  23364  2efiatan  23365  tanatan  23366  dvatan  23382  log2cnv  23391  log2ublem2  23394  log2ublem3  23395  basellem8  23478  ppi1  23555  cht1  23556  chp1  23558  ppi1i  23559  ppi2i  23560  cht2  23563  cht3  23564  bclbnd  23672  bposlem8  23683  ax5seglem7  24359  axlowdimlem8  24373  axlowdimlem11  24376  wlkntrllem2  24683  constr1trl  24711  constr2spthlem1  24717  constr3trllem3  24773  constr3pthlem1  24776  constr3pthlem3  24778  wlknwwlknvbij  24861  clwwlkvbij  24922  vdegp1ai  25105  ex-dif  25265  ex-xp  25278  ex-rn  25282  ip0i  25857  ip1ilem  25858  ipdirilem  25861  ipasslem10  25871  hvnegdii  26096  hvaddcani  26099  hvsubaddi  26100  hisubcomi  26138  normlem0  26143  normlem3  26146  normlem9  26152  bcseqi  26154  norm0  26162  norm-ii-i  26171  norm3difi  26181  normpari  26188  normpar2i  26190  polid2i  26191  shs0i  26484  chj0i  26490  pjsslem  26714  ho0subi  26830  hoaddsubi  26856  hosd1i  26857  hopncani  26859  nmop0  27021  nmfn0  27022  lnopunilem1  27045  lnophmlem2  27052  opsqrlem2  27176  pjclem1  27230  atabsi  27436  dmdbr6ati  27458  inin  27531  iuninc  27557  gtiso  27666  fpwrelmapffs  27707  ordtcnvNEW  28056  ordtrest2NEW  28059  zlmtset  28099  qqhucn  28126  zrhre  28150  qqhre  28151  esumnul  28196  mbfmcst  28386  carsggect  28445  eulerpartgbij  28494  eulerpartlemn  28503  fib0  28521  fib1  28522  fib2  28524  fib3  28525  fib4  28526  fib5  28527  fib6  28528  0rrv  28573  coinflipprob  28601  ballotlem2  28610  ballotlemfp1  28613  ballotth  28659  signsvf0  28720  derang0  28802  subfac0  28810  subfac1  28811  mthmpps  29131  problem2  29209  quad3  29213  dfrdg2  29393  pred0  29444  trpred0  29484  wfrlem14  29521  wfrlem16  29523  pprodcnveq  29686  dffv5  29727  fullfunfv  29750  ellines  29955  rankeq1o  29981  onint1  30067  mblfinlem2  30217  ismblfin  30220  dvtan  30231  asindmre  30268  dvasin  30269  dvacos  30270  areacirclem5  30277  heiborlem6  30478  diophrw  30857  dnwech  31160  lmhmlnmsplit  31199  fgraphopab  31338  arearect  31351  areaquad  31352  3lcm2e6  31387  hashnzfz  31393  lhe4.4ex1a  31402  sumnnodd  31802  cosnegpi  31833  itgsin0pilem1  31914  stoweidlem13  31961  wallispilem4  32016  wallispi2lem1  32019  wallispi2lem2  32020  stirlinglem3  32024  dirkertrigeqlem1  32046  fourierdlem56  32111  fourierdlem57  32112  fourierdlem58  32113  fourierdlem62  32117  fourierdlem103  32158  fourierdlem104  32159  fourierdlem112  32167  sqwvfoura  32177  fouriersw  32180  etransclem23  32206  etransclem36  32219  etransclem38  32221  5tcu2e40  32549  3exp4mod41  32550  41prothprmlem2  32552  41prothprm  32553  cznrnglem  32961  2t6m3t4e0  33137  zlmodzxzldeplem3  33303  sec0  33490  bnj1416  34442  bj-xpimasn  34860  bj-pr11val  34911  bj-pr21val  34919  bj-pr22val  34925  bj-nuliotaALT  34935  hdmap1cbv  37943  cnvtrrel  38207  dfrcl2  38211  dfrcl4  38215  relexpaddss  38223  comptiunov2i  38234  iunrelexp0  38242  corcltrcl  38249  cotrclrcl  38250  brtrclfv2  38258  xpheOLD  38276
  Copyright terms: Public domain W3C validator