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

Theorem 3eqtri 2449
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 2445 . 2  |-  B  =  D
51, 4eqtri 2445 1  |-  A  =  D
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-ext 2403
This theorem depends on definitions:  df-bi 188  df-cleq 2416
This theorem is referenced by:  csbid  3341  un23  3563  in32  3612  unvdif  3809  undif2  3811  undifabs  3812  difun2  3815  difdifdir  3823  dfif4  3864  dfif5  3865  tpidm23  4041  dfopif  4122  unisn  4172  dfiunv2  4273  symdif0  4314  symdifid  4316  unidif0  4535  uniop  4661  xpun  4849  dfrn2  4980  dfdmf  4985  dfrnf  5030  res0  5066  resres  5074  xpssres  5096  dfima2  5127  imai  5137  ima0  5140  imaundir  5206  xpima  5236  dmresv  5251  rescnvcnv  5255  dmtpop  5269  rnsnopg  5272  resdmres  5283  dmmpt  5287  dmco  5300  co01  5307  pred0  5367  suc0  5454  unisuc  5456  iunsuc  5462  fresaun  5709  dffv4  5817  fvssunirn  5843  fpr  6026  fvsnun2  6054  mpt20  6314  dmoprab  6330  rnoprab  6332  elrnmpt2res  6363  ov6g  6387  1st0  6752  2nd0  6753  dfmpt2  6836  curry1  6838  curry2  6841  fpar  6850  algrflem  6855  dftpos2  6940  tposoprab  6959  tposmpt2  6960  fvmpt2curryd  6968  wfrlem14  6999  wfrlem16  7001  dfrecs3  7041  tfrlem8  7052  seqomlem3  7119  df2o3  7145  omxpenlem  7621  dfsdom2  7643  marypha2lem2  7898  scottexs  8305  scott0s  8306  infxpenc2  8399  kmlem3  8528  cdaassen  8558  ackbij1lem2  8597  compsscnv  8747  fin1a2lem12  8787  mulerpqlem  9326  1lt2nq  9344  axi2m1  9529  2p2e4  10673  numsuc  11009  numsucc  11023  xnegmnf  11449  pnfaddmnf  11469  fz0tp  11839  fzo13pr  11942  fzo0to2pr  11943  fzo0to3tp  11944  fzo0to42pr  11945  i4  12322  crreczi  12342  fac1  12408  fac3  12411  hashkf  12462  hashinf  12465  dmhashres  12469  hashun3  12508  cshwsexa  12864  dmtrclfv  13021  abs0  13287  absi  13288  trirecip  13859  geoihalfsum  13876  esum  14073  tan0  14143  coshval  14147  ef01bndlem  14176  3dvds  14307  sadc0  14366  3lcm2e6woprm  14518  6lcm4e12  14519  lcmf0  14545  prmo0  14932  gcdmodi  14984  karatsuba  14994  43prm  15031  139prm  15033  631prm  15036  1259lem1  15040  1259lem2  15041  1259lem3  15042  1259lem4  15043  1259lem5  15044  2503lem1  15046  2503lem2  15047  2503lem3  15048  4001lem2  15051  4001lem3  15052  4001lem4  15053  4001prm  15054  ndxarg  15079  xpsc  15401  pmtrsn  17098  psgnprfval1  17101  sylow2a  17209  0frgp  17367  ablfac1eu  17644  sralem  18338  opsrtoslem2  18646  ply1plusgfvi  18773  pf1rcl  18875  restcld  20125  neitr  20133  txbasval  20558  txindis  20586  cnmpt1st  20620  cnmpt2nd  20621  ufildr  20883  restmetu  21522  reust  22277  ismbl  22417  mbfimaopnlem  22548  itg10  22583  itg2cnlem2  22657  itgz  22675  dvmptid  22848  cos2pi  23368  tan4thpi  23406  sincos6thpi  23407  pige3  23409  dfrelog  23452  logm1  23475  dvlog  23533  efopnlem2  23539  cxpexp  23550  root1id  23631  ang180lem2  23676  1cubrlem  23704  quart1  23719  atandm2  23740  efiasin  23751  asinsinlem  23754  asinsin  23755  asin1  23757  acos1  23758  atancj  23773  atanlogsublem  23778  efiatan2  23780  2efiatan  23781  tanatan  23782  dvatan  23798  log2cnv  23807  log2ublem2  23810  log2ublem3  23811  basellem8  23951  ppi1  24028  cht1  24029  chp1  24031  ppi1i  24032  ppi2i  24033  cht2  24036  cht3  24037  bclbnd  24145  bposlem8  24156  ax5seglem7  24902  axlowdimlem8  24916  axlowdimlem11  24919  wlkntrllem2  25227  constr1trl  25255  constr2spthlem1  25261  constr3trllem3  25317  constr3pthlem1  25320  constr3pthlem3  25322  wlknwwlknvbij  25405  clwwlkvbij  25466  vdegp1ai  25649  ex-dif  25810  ex-xp  25823  ex-rn  25827  ip0i  26403  ip1ilem  26404  ipdirilem  26407  ipasslem10  26417  hvnegdii  26652  hvaddcani  26655  hvsubaddi  26656  hisubcomi  26694  normlem0  26699  normlem3  26702  normlem9  26708  bcseqi  26710  norm0  26718  norm-ii-i  26727  norm3difi  26737  normpari  26744  normpar2i  26746  polid2i  26747  shs0i  27039  chj0i  27045  pjsslem  27269  ho0subi  27385  hoaddsubi  27411  hosd1i  27412  hopncani  27414  nmop0  27576  nmfn0  27577  lnopunilem1  27600  lnophmlem2  27607  opsqrlem2  27731  pjclem1  27785  atabsi  27991  dmdbr6ati  28013  inin  28087  iuninc  28117  gtiso  28222  fpwrelmapffs  28264  lmat22det  28595  ordtcnvNEW  28673  ordtrest2NEW  28676  zlmtset  28716  qqhucn  28743  zrhre  28770  qqhre  28771  esumnul  28816  mbfmcst  29028  carsggect  29097  eulerpartgbij  29152  eulerpartlemn  29161  fib0  29179  fib1  29180  fib2  29182  fib3  29183  fib4  29184  fib5  29185  fib6  29186  0rrv  29231  coinflipprob  29259  ballotlem2  29268  ballotlemfp1  29271  ballotth  29317  ballotthOLD  29355  signsvf0  29416  bnj1416  29795  derang0  29839  subfac0  29847  subfac1  29848  mthmpps  30167  problem2  30245  quad3  30249  dfrdg2  30388  trpred0  30423  pprodcnveq  30594  dffv5  30635  fullfunfv  30658  ellines  30863  rankeq1o  30882  onint1  31053  bj-xpimasn  31459  bj-pr11val  31510  bj-pr21val  31518  bj-pr22val  31524  bj-nuliotaALT  31534  icorempt2  31661  finxpreclem4  31693  finxp2o  31698  finxp3o  31699  poimirlem5  31852  poimirlem22  31869  poimirlem26  31873  poimirlem30  31877  mblfinlem2  31885  ismblfin  31888  dvtan  31899  asindmre  31934  dvasin  31935  dvacos  31936  areacirclem5  31943  heiborlem6  32055  hdmap1cbv  35283  diophrw  35513  dnwech  35819  lmhmlnmsplit  35858  fgraphopab  36000  arearect  36013  areaquad  36014  dmnonrel  36109  imanonrel  36112  cononrel1  36113  cononrel2  36114  rclexi  36135  dfrtrcl5  36149  cnvtrrel  36175  dfrcl2  36179  dfrcl4  36181  iunrelexp0  36207  comptiunov2i  36211  relexpaddss  36223  brtrclfv2  36232  trclfvdecomr  36233  corcltrcl  36244  cotrclrcl  36247  xpheOLD  36290  hashnzfz  36582  lhe4.4ex1a  36591  disjinfi  37372  sumnnodd  37593  cosnegpi  37625  itgsin0pilem1  37709  stoweidlem13  37756  wallispilem4  37813  wallispi2lem1  37816  wallispi2lem2  37817  stirlinglem3  37821  dirkertrigeqlem1  37843  fourierdlem56  37909  fourierdlem57  37910  fourierdlem58  37911  fourierdlem62  37915  fourierdlem103  37956  fourierdlem104  37957  fourierdlem112  37965  sqwvfoura  37975  fouriersw  37978  etransclem23  38005  etransclem36  38018  etransclem38  38020  carageniuncllem1  38193  0ome  38201  ovn02  38237  nnsum3primesgbe  38700  nnsum4primesodd  38704  nnsum4primesoddALTV  38705  nnsum4primeseven  38708  nnsum4primesevenALTV  38709  bgoldbtbndlem1  38713  tgoldbachlt  38722  5tcu2e40  38728  3exp4mod41  38729  41prothprmlem2  38731  41prothprm  38732  usgrexmpledg  39074  cznrnglem  39546  2t6m3t4e0  39722  zlmodzxzldeplem3  39888  sec0  40073
  Copyright terms: Public domain W3C validator