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

Theorem 3eqtri 2320
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 2316 . 2  |-  B  =  D
51, 4eqtri 2316 1  |-  A  =  D
Colors of variables: wff set class
Syntax hints:    = wceq 1632
This theorem is referenced by:  csbid  3101  un23  3347  in32  3394  dfrab2  3456  undifv  3541  undif2  3543  undifabs  3544  difun2  3546  difdifdir  3554  dfif4  3589  tpidm23  3743  dfopif  3809  unisn  3859  unidif0  4199  uniop  4285  suc0  4482  unisuc  4484  iunsuc  4490  xpun  4763  dfrn2  4884  dfdmf  4889  dfrnf  4933  res0  4975  resres  4984  xpssres  5005  dfima2  5030  imai  5043  ima0  5046  imaundir  5110  dmresv  5148  rescnvcnv  5151  dmtpop  5165  rnsnopg  5168  resdmres  5180  dmmpt  5184  dmco  5197  co01  5203  fresaun  5428  dffv4  5538  fvssunirn  5567  fpr  5720  fvsnun2  5732  dmoprab  5944  rnoprab  5946  ov6g  6001  1st0  6142  2nd0  6143  mpt20  6215  dfmpt2  6225  curry1  6226  curry2  6229  fpar  6238  algrflem  6240  dftpos2  6267  tposoprab  6286  tposmpt2  6287  tfrlem8  6416  seqomlem3  6480  df2o3  6508  omxpenlem  6979  dfsdom2  7000  marypha2lem2  7205  dfsup2OLD  7212  mapfien  7415  scottexs  7573  scott0s  7574  infxpenc2  7665  kmlem3  7794  cdaassen  7824  ackbij1lem2  7863  compsscnv  8013  fin1a2lem12  8053  mulerpqlem  8595  1lt2nq  8613  axi2m1  8797  2p2e4  9858  numsuc  10152  numsucc  10166  xnegmnf  10553  pnfaddmnf  10573  i4  11221  binom2aiOLD  11229  crreczi  11242  fac1  11308  fac3  11311  hashkf  11355  hashinf  11358  hashun3  11382  abs0  11786  absi  11787  trirecip  12337  geoihalfsum  12354  esum  12378  tan0  12447  coshval  12451  ef01bndlem  12480  3dvds  12607  sadc0  12661  gcdmodi  13105  karatsuba  13115  43prm  13139  139prm  13141  631prm  13144  1259lem1  13145  1259lem2  13146  1259lem3  13147  1259lem4  13148  1259lem5  13149  2503lem1  13151  2503lem2  13152  2503lem3  13153  4001lem2  13156  4001lem3  13157  4001lem4  13158  4001prm  13159  ndxarg  13184  xpsc  13475  sylow2a  14946  0frgp  15104  gsumval3  15207  gsumzaddlem  15219  ablfac1eu  15324  opsrtoslem2  16242  ply1plusgfvi  16336  restcld  16919  txbasval  17317  txindis  17344  cnmpt1st  17378  cnmpt2nd  17379  ufildr  17642  ismbl  18901  mbfimaopnlem  19026  itg10  19059  itg2cnlem2  19133  itgz  19151  dvmptid  19322  pf1rcl  19448  cos2pi  19860  tan4thpi  19898  sincos6thpi  19899  pige3  19901  dfrelog  19939  logm1  19958  dvlog  20014  efopnlem2  20020  cxpexp  20031  root1id  20110  ang180lem2  20124  1cubrlem  20153  quart1  20168  atandm2  20189  efiasin  20200  asinsinlem  20203  asinsin  20204  asin1  20206  acos1  20207  atancj  20222  atanlogsublem  20227  efiatan2  20229  2efiatan  20230  tanatan  20231  dvatan  20247  log2cnv  20256  log2ublem2  20259  log2ublem3  20260  basellem8  20341  ppi1  20418  cht1  20419  chp1  20421  ppi1i  20422  ppi2i  20423  cht2  20426  cht3  20427  bclbnd  20535  bposlem8  20546  ex-dif  20826  ex-xp  20839  ex-rn  20843  ip0i  21419  ip1ilem  21420  ipdirilem  21423  ipasslem10  21433  hvnegdii  21657  hvaddcani  21660  hvsubaddi  21661  hisubcomi  21699  normlem0  21704  normlem3  21707  normlem9  21713  bcseqi  21715  norm0  21723  norm-ii-i  21732  norm3difi  21742  normpari  21749  normpar2i  21751  polid2i  21752  shs0i  22044  chj0i  22050  pjsslem  22274  ho0subi  22391  hoaddsubi  22417  hosd1i  22418  hopncani  22420  nmop0  22582  nmfn0  22583  lnopunilem1  22606  lnophmlem2  22613  opsqrlem2  22737  pjclem1  22791  atabsi  22997  dmdbr6ati  23019  ballotlem2  23063  ballotlemfp1  23066  ballotth  23112  iuninc  23174  inin  23183  dmhashres  23190  xpima  23217  fmptpr  23229  gtiso  23256  esumnul  23442  mbfmcst  23579  0rrv  23669  derang0  23715  subfac0  23723  subfac1  23724  vdegp1ai  23923  dfrdg2  24223  pred0  24270  trpred0  24310  wfrlem14  24340  wfrlem16  24342  symdif0  24439  symdifid  24441  pprodcnveq  24494  dffv5  24534  fullfunfv  24557  ax5seglem7  24635  axlowdimlem8  24649  axlowdimlem11  24652  ellines  24847  rankeq1o  24873  onint1  24960  dvreasin  25026  areacirclem6  25033  inpc  25380  inposet  25381  ranncnt  25386  dispos  25390  trnij  25718  dfiunv2  26019  cmp2morpdom  26067  cmp2morpcod  26068  intset  26147  heiborlem6  26643  diophrw  26941  dnwech  27248  lmhmlnmsplit  27288  fgraphopab  27632  lhe4.4ex1a  27649  stoweidlem13  27865  wallispi2lem1  27923  wallispi2lem2  27924  stirlinglem3  27928  fzo0to3tp  28210  fzo0to42pr  28211  wlkntrllem4  28348  usgrcyclnl2  28387  constr3trllem3  28398  constr3pthlem1  28401  constr3pthlem3  28403  sec0  28484  bnj1416  29385  hdmap1cbv  32615
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-cleq 2289
  Copyright terms: Public domain W3C validator