Theorem 3eqtri 1542

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 1538	. 2 |- B = D
5	1, 4	eqtri 1538	1 |- A = D

Syntax hints:   = wceq 992

This theorem is referenced by:  csbid 2056  dfrab2 2326  difin0 2391  undifv 2392  undif1 2393  undif2 2394  inundif 2395  difun2 2396  difdifdir 2400  pwpr 2567  unisn 2583  intsn 2631  iunid 2671  2iunin 2680  unidif0 2813  uniop 2885  dfid3 2914  suc0 3047  unisuc 3049  op1stb 3136  orduniss2 3187  xpun 3312  dfrn2 3394  dfdmf 3397  dfrnf 3435  res0 3458  resres 3464  resopab 3485  dfima2 3497  imai 3509  ima0 3512  imaundir 3546  resdisj 3556  rnsnop 3582  dmresv 3588  rescnvcnv 3591  resdmres 3595  dfco2a 3599  dmco 3607  fvsnun1 3907  fvsnun2 3908  fopabap 3955  dmoprab 4062  rnoprab 4064  oprabval6g 4093  1st0 4144  2nd0 4145  curry1 4193  curry2 4196  fparlem1 4199  fparlem3 4201  fparlem4 4202  fpar 4203  tfrlem8 4219  tz7.44-1 4229  df2o2 4277  ecid 4441  qsid 4442  sbthlem5 4596  dfsdom2 4605  mapenlem2 4637  rankpr 4838  rankop 4839  ranksuc 4846  scottexs 4864  scott0s 4865  hta 4874  kmlem3 4913  cda0en 5077  supsrlem2 5380  axmulass 5432  axi2m1 5439  negsubi 5535  mulneg1i 5599  mulneg2i 5600  mul2negi 5601  negsubdi2i 5604  ltsubaddi 5748  ltnegi 5757  divreci 5883  div23i 5894  rec11ii 5916  prodgt0lem 5958  nnsubi 6102  2p2e4 6147  3t3e9 6170  8th4div3 6177  seq11lem 6680  seq0seqz 6737  seq00 6745  cu2 6837  binom2i 6841  binom2aiOLD 6842  discrlem1 6857  nnesqi 6863  sqr0 6873  sqrlem11 6884  sqrlem16 6889  i3 6934  i4 6935  crulem 6937  crmuli 6941  crreczi 6942  cjcji 6979  addcji 6999  absi 7081  abslem2i 7111  fac1 7138  fac2 7140  fac3 7141  bcpasc2i 7170  binomlem6 7274  iserzshfti 7347  arisumi 7430  geolim1i 7443  0.999... 7451  eval 7514  erelem6 7529  ege2lem2 7533  ege2le3lem2 7534  efcji 7541  efaddlem6 7548  efaddlem16 7558  eirrlem1 7594  eft0vali 7606  ef4pi 7607  efge1pi 7610  sin0 7652  cos0 7654  sinaddi 7659  cosaddi 7660  sin01bndlem1 7676  acdc2lem2 7701  acdc5lem2 7704  ruclem6 7727  ruclem12 7733  ruclem15 7736  infmap2lem1 7791  subtop 7858  indistps 7863  remetba 8120  grpidvallem 8274  vsfval 8501  nvpi 8541  ipval2 8611  ip0i 8740  ip1ilem 8741  ip2i 8743  ipdirilem 8744  ipasslem10 8755  spwval2 8915  pilem3 8940  eulerid 8950  sin2pi 8951  cos2pi 8952  sincosq4sgn 8974  sincos6thpi 8979  dfrelog 9028  pilog 9040  hvnegdii 9204  hvsubeq0i 9205  hvsubcan2i 9206  hvaddcani 9207  hvsubaddi 9208  hisubcomi 9246  normlem0 9251  normlem1 9252  normlem3 9254  normlem9 9260  bcseqi 9262  norm0 9271  norm-ii.i 9280  normsubi 9284  norm3difi 9290  normpari 9297  normpar2i 9299  polid2i 9300  hhshsslem1 9413  projlem3 9464  projlem4 9465  pjthlem5 9499  pjthlem13 9507  shs0i 9648  chj0i 9654  pjoml2i 9804  osumcor2i 9868  pjsslem 9902  pjssmii 9904  ho0subi 10001  hoaddsubi 10027  hosd1i 10028  hopncani 10030  hosubeq0i 10032  hhbloi 10108  hh0oi 10109  nmop0 10189  nmfn0 10190  lnopunilem1 10214  lnophmlem2 10221  pjclem1 10404  pjcmmul1i 10410  cvmdi 10532  mdexchi 10543  atabsi 10610  dmdbr6ati 10632  symgval 10688  cmpbva 10748  cmpran 10753  prj1 10809  inpc 10867  inposet 10868  domncnt 10872  ranncnt 10873  empos 10875  dispos 10881  stoiglem 11063  intopcon 11133  singempcon 11134  stoi 11145  trnij 11160  1cat 11213  subcld 11480  filcon 11665  gapm 11784  fsumltisumi 11886  trirni 11896  piececn 11955  tx1cn 11976  tx2cn 11977  bfplem2 12055

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 999  ax-17 1007  ax-4 1009  ax-5o 1011  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-cleq 1511

Copyright terms: Public domain