Theorem 3eqtr 1491

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

Step	Hyp	Ref	Expression
1		3eqtr.1	. 2 |- A = B
2		3eqtr.2	. . 3 |- B = C
3		3eqtr.3	. . 3 |- C = D
4	2, 3	eqtr 1487	. 2 |- B = D
5	1, 4	eqtr 1487	1 |- A = D

Syntax hints:   = wceq 953

This theorem is referenced by:  csbid 1995  dfrab2 2264  difin0 2328  undifv 2329  undif1 2330  undif2 2331  difun2 2332  difdifdir 2336  unisn 2507  intsn 2554  unidif0 2729  uniop 2797  dfid3 2826  op1stb 2903  suc0 3033  unisuc 3036  orduniss2 3080  xpun 3217  dfrn2 3292  dfdmf 3295  dfrnf 3334  res0 3355  resres 3361  resopab 3379  dfima2 3389  imai 3401  ima0 3404  rnsnop 3436  imaun2 3447  resdisj 3457  dmresv 3476  rescnvcnv 3479  resdmres 3483  dmco2 3490  fvsnun1 3780  fvsnun2 3781  fopabap 3826  tfrlem8 3903  tz7.44-1 3913  dmoprab 3987  rnoprab 3989  oprabval6g 4017  1st0 4067  2nd0 4068  curry1 4082  df2o2 4125  ecid 4284  qsid 4285  sbthlem5 4431  dfsdom2 4440  mapenlem2 4470  rankpr 4664  rankop 4665  ranksuc 4672  scottexs 4690  scott0s 4691  hta 4700  kmlem3 4739  cda0en 4897  supsrlem2 5198  axmulass 5250  axi2m1 5257  negsub 5353  mulneg1 5417  mulneg2 5418  mul2neg 5419  negsubdi2 5422  ltsubadd 5568  ltneg 5577  divrec 5700  div23 5711  rec11i 5733  prodgt0lem 5774  nnsub 5903  2p2e4 5948  3t3e9 5971  8th4div3 5978  seq11lem 6252  seq0seqz 6474  seq00 6482  cu2 6571  binom2 6575  binom2aOLD 6576  discrlem1 6586  nnesq 6592  sqr0 6602  sqrlem11 6613  sqrlem16 6618  i3 6663  i4 6664  crulem 6666  crmul 6671  crrecz 6672  imret 6710  cjcj 6713  addcj 6733  absi 6815  abslem2i 6845  fac1 6872  fac2 6874  fac3 6875  bcpasc2 6905  binomlem6 7009  iserzshft 7080  fnsmnt 7161  geolim1i 7173  0.999... 7181  eval 7251  erelem6 7266  ege2lem2 7270  ege2le3lem2 7271  efcj 7278  efaddlem6 7285  efaddlem16 7295  eirrlem1 7330  eft0val 7339  ef4p 7340  efge1p 7343  sin0 7386  cos0 7388  sinadd 7393  cosadd 7394  sin01bndlem1 7409  acdc2lem2 7431  acdc5lem2 7434  ruclem6 7458  ruclem12 7464  ruclem15 7467  infmap2lem1 7521  subtop 7588  indistps 7595  remetba 7848  vsfval 8194  nvpi 8233  ipval2 8291  ip0i 8415  ip1ilem 8416  ip2i 8418  ipdirilem 8419  ipasslem10 8430  spwval2 8577  pilem3 8592  eulerid 8602  sin2pi 8603  cos2pi 8604  sincosq4sgn 8624  sincos6thpi 8628  dfrelog 8678  pilog 8690  hvnegdi 8850  hvsubeq0 8851  hvsubcan2 8852  hvaddcan 8853  hvsubadd 8854  hisubcom 8891  normlem0 8896  normlem1 8897  normlem3 8899  normlem9 8905  bcseq 8907  norm0 8916  norm-ii 8925  normsub 8929  norm3dif 8935  normpar 8942  normpar2 8944  polid2 8945  hhshsslem1 9057  projlem3 9104  projlem4 9105  pjthlem5 9138  pjthlem13 9146  shs0 9287  chj0 9293  pjoml2 9445  osumcor2 9507  pjsslem 9541  pjssm 9543  ho0sub 9638  hoaddsub 9664  hosd1 9665  hopncan 9667  hosubeq0 9669  hhblo 9745  hh0o 9746  nmop0 9826  nmfn0 9827  lnopunilem1 9850  lnophmlem2 9857  pjclem1 10033  pjcmmul1 10039  cvmd 10159  mdexch 10170  atabs 10236  dmdbr6at 10256  symgval 10308  cmpbva 10360  cmpran 10365  trnij 10481  stoi 10483  1cat 10536

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1462

Copyright terms: Public domain