HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem 3eqtr 1496
Description: An inference from three chained equalities.
Hypotheses
Ref Expression
3eqtr.1 |- A = B
3eqtr.2 |- B = C
3eqtr.3 |- C = D
Assertion
Ref Expression
3eqtr |- A = D
Proof of Theorem 3eqtr
StepHypRef Expression
1 3eqtr.1 . 2 |- A = B
2 3eqtr.2 . . 3 |- B = C
3 3eqtr.3 . . 3 |- C = D
42, 3eqtr 1492 . 2 |- B = D
51, 4eqtr 1492 1 |- A = D
Colors of variables: wff set class
Syntax hints:   = wceq 954
This theorem is referenced by:  csbid 2001  dfrab2 2270  difin0 2334  undifv 2335  undif1 2336  undif2 2337  difun2 2338  difdifdir 2342  unisn 2512  intsn 2559  unidif0 2734  uniop 2803  dfid3 2831  op1stb 2908  suc0 3038  unisuc 3041  orduniss2 3085  xpun 3222  dfrn2 3298  dfdmf 3301  dfrnf 3342  res0 3363  resres 3369  resopab 3387  dfima2 3397  imai 3409  ima0 3412  rnsnop 3442  imaun2 3453  resdisj 3463  dmresv 3482  rescnvcnv 3485  resdmres 3489  dmco2 3496  fvsnun1 3786  fvsnun2 3787  fopabap 3832  tfrlem8 3909  tz7.44-1 3919  dmoprab 3993  rnoprab 3995  oprabval6g 4023  1st0 4073  2nd0 4074  curry1 4088  df2o2 4131  ecid 4290  qsid 4291  sbthlem5 4437  dfsdom2 4446  mapenlem2 4476  rankpr 4672  rankop 4673  ranksuc 4680  scottexs 4698  scott0s 4699  hta 4708  kmlem3 4747  cda0en 4905  supsrlem2 5206  axmulass 5258  axi2m1 5265  negsub 5361  mulneg1 5425  mulneg2 5426  mul2neg 5427  negsubdi2 5430  ltsubadd 5576  ltneg 5585  divrec 5708  div23 5719  rec11i 5741  prodgt0lem 5782  nnsub 5911  2p2e4 5956  3t3e9 5979  8th4div3 5986  seq11lem 6260  seq0seqz 6482  seq00 6490  cu2 6579  binom2 6583  binom2aOLD 6584  discrlem1 6594  nnesq 6600  sqr0 6610  sqrlem11 6621  sqrlem16 6626  i3 6671  i4 6672  crulem 6674  crmul 6679  crrecz 6680  imret 6718  cjcj 6721  addcj 6741  absi 6823  abslem2i 6853  fac1 6880  fac2 6882  fac3 6883  bcpasc2 6913  binomlem6 7017  iserzshft 7088  fnsmnt 7169  geolim1i 7181  0.999... 7189  eval 7259  erelem6 7274  ege2lem2 7278  ege2le3lem2 7279  efcj 7286  efaddlem6 7293  efaddlem16 7303  eirrlem1 7338  eft0val 7347  ef4p 7348  efge1p 7351  sin0 7394  cos0 7396  sinadd 7401  cosadd 7402  sin01bndlem1 7417  acdc2lem2 7439  acdc5lem2 7442  ruclem6 7466  ruclem12 7472  ruclem15 7475  infmap2lem1 7529  subtop 7596  indistps 7603  remetba 7861  vsfval 8206  nvpi 8246  ipval2 8304  ip0i 8428  ip1ilem 8429  ip2i 8431  ipdirilem 8432  ipasslem10 8443  spwval2 8595  pilem3 8611  eulerid 8621  sin2pi 8622  cos2pi 8623  sincosq4sgn 8643  sincos6thpi 8647  dfrelog 8695  pilog 8707  hvnegdi 8868  hvsubeq0 8869  hvsubcan2 8870  hvaddcan 8871  hvsubadd 8872  hisubcom 8909  normlem0 8914  normlem1 8915  normlem3 8917  normlem9 8923  bcseq 8925  norm0 8934  norm-ii 8943  normsub 8947  norm3dif 8953  normpar 8960  normpar2 8962  polid2 8963  hhshsslem1 9076  projlem3 9127  projlem4 9128  pjthlem5 9161  pjthlem13 9169  shs0 9310  chj0 9316  pjoml2 9468  osumcor2 9530  pjsslem 9564  pjssm 9566  ho0sub 9661  hoaddsub 9687  hosd1 9688  hopncan 9690  hosubeq0 9692  hhblo 9768  hh0o 9769  nmop0 9849  nmfn0 9850  lnopunilem1 9873  lnophmlem2 9880  pjclem1 10061  pjcmmul1 10067  cvmd 10188  mdexch 10199  atabs 10265  dmdbr6at 10285  symgval 10337  cmpbva 10396  cmpran 10401  trnij 10517  stoi 10519  1cat 10572
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-17 969  ax-4 971  ax-5o 973  ax-ext 1457
This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1467
Copyright terms: Public domain