Theorem 3tr 65

Description: Triple transitive inference. (Contributed by NM, 20-Sep-1998.)

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 was proved from axioms:  ax-r2 36

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  ska2  432  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  1041  lem3.3.3  1052  lem3.3.4  1053  lem3.3.7i0e1  1057  lem3.3.7i1e1  1060  lem3.3.7i1e2  1061  lem3.3.7i2e1  1063  lem3.3.7i2e2  1064  lem3.3.7i3e1  1066  lem3.3.7i3e2  1067  lem3.3.7i4e1  1069  lem3.3.7i4e2  1070  lem3.3.7i5e1  1072  lem3.4.6  1079  lem4.6.2e1  1082  lem4.6.6i1j3  1094  lem4.6.6i2j4  1097  lem4.6.6i3j0  1098  lem4.6.6i3j1  1099  lem4.6.6i4j2  1101  wdcom  1105  mldual  1124  mli  1126  mlduali  1128  ml3le  1129  vneulem2  1132  vneulem4  1134  vneulem5  1135  vneulem9  1139  vneulem11  1141  vneulem13  1143  vneulem16  1146  vneulemexp  1148  l42modlem1  1149  dp15lema  1154  dp15lemd  1157  dp53lemb  1164  dp53lemc  1165  dp53leme  1167  dp35lemc  1175  dp35lemb  1176  dp41lemc0  1184  dp41lemd  1186  dp41leme  1187  dp41lemf  1188  dp41lemg  1189  dp41leml  1193  dp41lemm  1194  dp32  1196  xdp41  1198  xdp15  1199  xdp53  1200  xxdp41  1201  xxdp15  1202  xxdp53  1203  xdp45lem  1204  xdp43lem  1205  xdp45  1206  xdp43  1207  3dp43  1208  oadp35lemc  1211  testmod  1213