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

Theorem 3eqtri 2428
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 2424 . 2  |-  B  =  D
51, 4eqtri 2424 1  |-  A  =  D
Colors of variables: wff set class
Syntax hints:    = wceq 1649
This theorem is referenced by:  csbid  3218  un23  3466  in32  3513  dfrab2  3576  undifv  3662  undif2  3664  undifabs  3665  difun2  3667  difdifdir  3675  dfif4  3710  dfif5  3711  tpidm23  3867  dfopif  3941  unisn  3991  dfiunv2  4087  unidif0  4332  uniop  4419  suc0  4615  unisuc  4617  iunsuc  4623  xpun  4894  dfrn2  5018  dfdmf  5023  dfrnf  5067  res0  5109  resres  5118  xpssres  5139  dfima2  5164  imai  5177  ima0  5180  imaundir  5244  xpima  5272  dmresv  5288  rescnvcnv  5291  dmtpop  5305  rnsnopg  5308  resdmres  5320  dmmpt  5324  dmco  5337  co01  5343  fresaun  5573  dffv4  5684  fvssunirn  5713  fpr  5873  fvsnun2  5888  dmoprab  6113  rnoprab  6115  ov6g  6170  1st0  6312  2nd0  6313  mpt20  6386  dfmpt2  6396  curry1  6397  curry2  6400  fpar  6409  algrflem  6414  dftpos2  6455  tposoprab  6474  tposmpt2  6475  tfrlem8  6604  seqomlem3  6668  df2o3  6696  omxpenlem  7168  dfsdom2  7189  marypha2lem2  7399  dfsup2OLD  7406  mapfien  7609  scottexs  7767  scott0s  7768  infxpenc2  7859  kmlem3  7988  cdaassen  8018  ackbij1lem2  8057  compsscnv  8207  fin1a2lem12  8247  mulerpqlem  8788  1lt2nq  8806  axi2m1  8990  2p2e4  10054  numsuc  10350  numsucc  10364  xnegmnf  10752  pnfaddmnf  10772  fz0tp  11059  fzo0to2pr  11139  fzo0to3tp  11140  fzo0to42pr  11141  i4  11438  binom2aiOLD  11446  crreczi  11459  fac1  11525  fac3  11528  hashkf  11575  hashinf  11578  hashun3  11613  abs0  12045  absi  12046  trirecip  12597  geoihalfsum  12614  esum  12638  tan0  12707  coshval  12711  ef01bndlem  12740  3dvds  12867  sadc0  12921  gcdmodi  13365  karatsuba  13375  43prm  13399  139prm  13401  631prm  13404  1259lem1  13405  1259lem2  13406  1259lem3  13407  1259lem4  13408  1259lem5  13409  2503lem1  13411  2503lem2  13412  2503lem3  13413  4001lem2  13416  4001lem3  13417  4001lem4  13418  4001prm  13419  ndxarg  13444  xpsc  13737  sylow2a  15208  0frgp  15366  gsumval3  15469  gsumzaddlem  15481  ablfac1eu  15586  opsrtoslem2  16500  ply1plusgfvi  16591  restcld  17190  neitr  17198  txbasval  17591  txindis  17619  cnmpt1st  17653  cnmpt2nd  17654  ufildr  17916  restmetu  18570  ismbl  19375  mbfimaopnlem  19500  itg10  19533  itg2cnlem2  19607  itgz  19625  dvmptid  19796  pf1rcl  19922  cos2pi  20337  tan4thpi  20375  sincos6thpi  20376  pige3  20378  dfrelog  20416  logm1  20436  dvlog  20495  efopnlem2  20501  cxpexp  20512  root1id  20591  ang180lem2  20605  1cubrlem  20634  quart1  20649  atandm2  20670  efiasin  20681  asinsinlem  20684  asinsin  20685  asin1  20687  acos1  20688  atancj  20703  atanlogsublem  20708  efiatan2  20710  2efiatan  20711  tanatan  20712  dvatan  20728  log2cnv  20737  log2ublem2  20740  log2ublem3  20741  basellem8  20823  ppi1  20900  cht1  20901  chp1  20903  ppi1i  20904  ppi2i  20905  cht2  20908  cht3  20909  bclbnd  21017  bposlem8  21028  wlkntrllem2  21513  constr1trl  21541  constr2spthlem1  21547  constr3trllem3  21592  constr3pthlem1  21595  constr3pthlem3  21597  vdegp1ai  21659  ex-dif  21684  ex-xp  21697  ex-rn  21701  ip0i  22279  ip1ilem  22280  ipdirilem  22283  ipasslem10  22293  hvnegdii  22517  hvaddcani  22520  hvsubaddi  22521  hisubcomi  22559  normlem0  22564  normlem3  22567  normlem9  22573  bcseqi  22575  norm0  22583  norm-ii-i  22592  norm3difi  22602  normpari  22609  normpar2i  22611  polid2i  22612  shs0i  22904  chj0i  22910  pjsslem  23134  ho0subi  23251  hoaddsubi  23277  hosd1i  23278  hopncani  23280  nmop0  23442  nmfn0  23443  lnopunilem1  23466  lnophmlem2  23473  opsqrlem2  23597  pjclem1  23651  atabsi  23857  dmdbr6ati  23879  inin  23949  iuninc  23964  fmptpr  24015  gtiso  24041  dmhashres  24110  reust  24297  zlmtset  24302  qqhucn  24329  rrhcn  24333  zrhre  24338  qqhre  24339  rrhre  24340  esumnul  24396  mbfmcst  24562  0rrv  24662  coinflipprob  24690  ballotlem2  24699  ballotlemfp1  24702  ballotth  24748  derang0  24808  subfac0  24816  subfac1  24817  dfrdg2  25366  pred0  25413  trpred0  25453  wfrlem14  25483  wfrlem16  25485  symdif0  25582  symdifid  25584  pprodcnveq  25637  dffv5  25677  fullfunfv  25700  ax5seglem7  25778  axlowdimlem8  25792  axlowdimlem11  25795  ellines  25990  rankeq1o  26016  onint1  26103  mblfinlem  26143  ismblfin  26146  dvreasin  26179  areacirclem6  26186  heiborlem6  26415  diophrw  26707  dnwech  27013  lmhmlnmsplit  27053  fgraphopab  27397  lhe4.4ex1a  27414  itgsin0pilem1  27611  stoweidlem13  27629  wallispilem4  27684  wallispi2lem1  27687  wallispi2lem2  27688  stirlinglem3  27692  sec0  28217  bnj1416  29114  hdmap1cbv  32286
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2397
  Copyright terms: Public domain W3C validator