Theorem 3eqtri 1912

Description: An inference from three chained equalities.

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

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

Syntax hints:   = wceq 1298

This theorem is referenced by:  csbid 2545  un23 2762  in23 2806  dfrab2 2869  difin0OLD 2947  undifv 2948  undif1 2949  undif2 2950  inundifOLD 2952  difun2 2953  difdifdir 2957  pwpr 3174  unisn 3193  intsn 3252  iunid 3308  2iunin 3323  unidif0 3476  uniop 3555  dfid3 3587  suc0 3739  unisuc 3741  op1stb 3857  orduniss2 3913  xpun 4052  dfrn2 4149  dfdmf 4152  dfrnf 4195  res0 4221  resres 4228  resopab 4252  dfima2 4265  dfima2OLD 4266  imai 4280  ima0 4283  imaundir 4329  resdisjOLD 4341  dmtpop 4370  rnsnop 4375  dmresv 4382  rescnvcnv 4385  rescnvcnvOLD 4386  resdmres 4390  dfco2aOLD 4395  dmco 4406  fvsnun1 4764  fvsnun2 4765  fpr 4810  fprOLD 4811  fopabap 4817  dmoprab 4931  rnoprab 4933  oprabval6g 4962  1st0 5024  2nd0 5025  curry1 5075  curry2 5078  fparlem1 5081  fparlem3 5083  fparlem4 5084  fpar 5085  tfrlem8 5126  tz7.44-1 5136  df2o2 5186  ecid 5359  qsid 5360  sbthlem5 5514  dfsdom2 5523  mapenlem2 5584  rankpr 5803  rankop 5804  ranksuc 5811  scottexs 5848  scott0s 5849  hta 5858  kmlem3 5929  cda0en 6075  supsrlem2 6378  axmulass 6431  axi2m1 6438  negsubi 6538  negsubiOLD 6539  mulneg1i 6608  mulneg2i 6609  mul2negi 6610  negsubdi2i 6614  ltsubaddiOLD 6770  ltnegi 6783  divreci 6920  div23i 6931  rec11ii 6953  prodgt0lem 6996  nnsubi 7140  2p2e4 7185  3t3e9 7208  8th4div3 7217  seq11lem 7728  seq0seqz 7785  seq00 7793  cu2 7885  binom2i 7890  binom2aiOLD 7891  discrlem1 7906  nnesqi 7912  sqr0 7922  sqrlem11 7933  sqrlem16 7938  i3 7983  i4 7984  crulem 7986  crmuli 7990  crreczi 7991  cjcji 8028  addcji 8048  absi 8130  abslem2i 8160  fac1 8187  fac2 8189  fac3 8190  bcpasc2i 8219  binomlem6 8331  iserzshfti 8404  arisumi 8487  geolim1i 8500  0.999... 8508  eval 8571  erelem6 8586  ege2lem2 8590  ege2le3lem2 8591  efcji 8598  efaddlem6 8605  efaddlem16 8615  eirrlem1 8651  eft0vali 8663  ef4pi 8664  efge1pi 8667  sin0 8709  cos0 8711  sinaddi 8716  cosaddi 8717  sin01bndlem1 8733  acdc2lem2 8758  acdc5lem2 8761  ruclem6 8784  ruclem12 8790  ruclem15 8793  infmap2lem1 8848  subtop 8916  indistps 8923  remetba 9187  grpidvallem 9341  gapm 9462  vsfval 9586  nvpi 9626  ipval2 9696  ip0i 9825  ip1ilem 9826  ip2i 9828  ipdirilem 9829  ipasslem10 9840  spwval2 9996  pilem3 10022  eulerid 10032  sin2pi 10033  cos2pi 10034  sincosq4sgn 10056  sincos6thpi 10061  dfrelog 10110  pilog 10122  symgval 10202  tx1cn 10223  tx2cn 10224  stoiglem 10250  subcld 10254  hvnegdii 10561  hvsubeq0i 10562  hvsubcan2i 10563  hvaddcani 10564  hvsubaddi 10565  hisubcomi 10603  normlem0 10608  normlem1 10609  normlem3 10611  normlem9 10617  bcseqi 10619  norm0 10628  norm-ii.i 10637  normsubi 10641  norm3difi 10647  normpari 10654  normpar2i 10656  polid2i 10657  hhshsslem1 10770  projlem3 10821  projlem4 10822  pjthlem5 10856  pjthlem13 10864  shs0i 11005  chj0i 11011  pjoml2i 11161  osumcor2i 11225  pjsslem 11259  pjssmii 11261  ho0subi 11358  hoaddsubi 11384  hosd1i 11385  hopncani 11387  hosubeq0i 11389  hhbloi 11465  hh0oi 11466  nmop0 11547  nmfn0 11548  lnopunilem1 11572  lnophmlem2 11579  opsqrlem2 11712  pjclem1 11768  pjcmmul1i 11774  cvmdi 11896  mdexchi 11907  atabsi 11973  dmdbr6ati 11995  bnj1398 13515  bnj1416 13528  pred0 13910  wfrlem14 13970  wfrlem16 13972  prj1 14395  cmpbvb 14477  cmpran 14483  rngop 14484  repfuntw 14502  empos 14583  inpc 14619  inposet 14620  domncnt 14624  ranncnt 14625  dispos 14632  dfdir2 14639  cmprtr 14760  prtoptop 14919  intopcon 14964  singempcon 14965  idtrgrp 14978  trhom 14983  stoi 14998  cntrsetlem 14999  trnij 15015  1cat 15106  filcon 15580  fsumltisumi 15823  trirni 15833  piececn 15894  txmet 15925  bfplem2 15999  pcopt 16084  pcoass 16085  stb2xpl 16742  stb3xpl 16743

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-cleq 1877

Copyright terms: Public domain