Theorem 3tr 62

Description: Triple transitive inference.

Hypotheses

Ref	Expression
3tr.1	a = b
3tr.2	b = c
3tr.3	c = d

Assertion

Ref	Expression
3tr	a = d

Proof of Theorem 3tr

Step	Hyp	Ref	Expression
1		3tr.1	. . 3 a = b
2		3tr.2	. . 3 b = c
3	1, 2	ax-r2 35	. 2 a = c
4		3tr.3	. 2 c = d
5	3, 4	ax-r2 35	1 a = d

Syntax hints:   = wb 1

This theorem is referenced by:  0i1 265  wql2lem2 281  wql2lem3 282  wql2lem4 283  wql2lem5 284  wql1 285  nom14 303  nom15 304  nom22 307  nom55 328  2vwomlem 347  wdf-c1 365  ska4 415  woml6 418  woml7 419  oml6 470  gsth 471  i0cmtrcom 477  u12lembi 708  u21lembi 709  oi3oa3lem1 714  oi3oa3 715  u1lem8 758  u1lem11 762  u3lem15 777  bi1o1a 780  i2i1i1 782  i1abs 783  3vth7 792  3vded11 796  3vded21 799  3vded3 801  1oa 802  2oalem1 807  2oath1 808  oale 811  3vroa 813  mlalem 814  mlaoml 815  sa5 818  salem1 819  bi3 821  bi4 822  imp3 823  orbi 824  mlaconj4 826  mlaconj 827  neg3antlem2 847  elimcons2 851  comanblem1 852  comanblem2 853  mhlemlem1 856  mhlem 858  mhlem1 859  mh 861  marsdenlem2 863  marsdenlem3 864  marsdenlem4 865  mlaconjolem 867  mlaconjo 868  mhcor1 870  cancellem 873  govar 876  gomaex4 880  go2n6 881  gomaex3lem1 894  gomaex3lem3 896  gomaex3lem7 900  gomaex3lem9 902  oau 909  oa4v3v 914  oa23 916  oa6to4 938  oa8to5 952  oa4to4u 953  oa3-2lema 958  oa3-6lem 960  oa3-1lem 962  oa3-5lem 964  oa3-u1lem 965  oa3-u1 971  oa3-u2 972  oath1 984  oalem2 986  oacom3 993  4oath1 1020

This theorem was proved from axioms:  ax-r2 35

metamath.org