Theorem 3tr 65

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 36	. 2 a = c
4		3tr.3	. 2 c = d
5	3, 4	ax-r2 36	1 a = d

Syntax hints:   = wb 1

This theorem is referenced by:  0i1 273  wql2lem2 289  wql2lem3 290  wql2lem4 291  wql2lem5 292  wql1 293  nom14 311  nom15 312  nom22 315  nom55 336  k1-6 353  k1-7 354  k1-8a 355  k1-8b 356  k1-4 359  2vwomlem 365  wdf-c1 383  ska4 433  woml6 436  woml7 437  oml6 488  gsth 489  i0cmtrcom 495  ud1lem2 561  u12lembi 726  u21lembi 727  oi3oa3lem1 732  oi3oa3 733  u1lem8 776  u1lem11 780  u3lem15 795  bi1o1a 798  i2i1i1 800  i1abs 801  3vth7 810  3vded11 814  3vded21 817  3vded3 819  1oa 820  2oalem1 825  2oath1 826  oale 829  3vroa 831  mlalem 832  mlaoml 833  sa5 836  salem1 837  bi3 839  bi4 840  imp3 841  orbi 842  mlaconj4 844  mlaconj 845  neg3antlem2 865  elimcons2 869  comanblem1 870  comanblem2 871  mhlemlem1 874  mhlem 876  mhlem1 877  mh 879  marsdenlem2 881  marsdenlem3 882  marsdenlem4 883  mlaconjolem 885  mlaconjo 886  mhcor1 888  cancellem 891  e2ast2 894  e2astlem1 895  govar 896  gomaex4 900  go2n6 901  gomaex3lem1 914  gomaex3lem3 916  gomaex3lem7 920  gomaex3lem9 922  oau 929  oa4v3v 934  oa23 936  oa6to4 958  oa8to5 972  oa4to4u 973  oa3-2lema 978  oa3-6lem 980  oa3-1lem 982  oa3-5lem 984  oa3-u1lem 985  oa3-u1 991  oa3-u2 992  oath1 1004  oalem2 1006  oacom3 1013  4oath1 1040  lem3.3.3 1051  lem3.3.4 1052  lem3.3.7i0e1 1056  lem3.3.7i1e1 1059  lem3.3.7i1e2 1060  lem3.3.7i2e1 1062  lem3.3.7i2e2 1063  lem3.3.7i3e1 1065  lem3.3.7i3e2 1066  lem3.3.7i4e1 1068  lem3.3.7i4e2 1069  lem3.3.7i5e1 1071  lem3.4.6 1078  lem4.6.2e1 1079  lem4.6.6i1j3 1091  lem4.6.6i2j4 1094  lem4.6.6i3j0 1095  lem4.6.6i3j1 1096  lem4.6.6i4j2 1098  wdcom 1102

This theorem was proved from axioms:  ax-r2 36

Copyright terms: Public domain