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 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  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  1080  lem4.6.6i1j3  1092  lem4.6.6i2j4  1095  lem4.6.6i3j0  1096  lem4.6.6i3j1  1097  lem4.6.6i4j2  1099  wdcom  1103  mldual  1122  mli  1124  mlduali  1126  ml3le  1127  vneulem2  1130  vneulem4  1132  vneulem5  1133  vneulem9  1137  vneulem11  1139  vneulem13  1141  vneulem16  1144  vneulemexp  1146  l42modlem1  1147  dp15lema  1152  dp15lemd  1155  dp53lemb  1162  dp53lemc  1163  dp53leme  1165  dp35lemc  1173  dp35lemb  1174  dp41lemc0  1182  dp41lemd  1184  dp41leme  1185  dp41lemf  1186  dp41lemg  1187  dp41leml  1191  dp41lemm  1192  dp32  1194  xdp41  1196  xdp15  1197  xdp53  1198  xxdp41  1199  xxdp15  1200  xxdp53  1201  xdp45lem  1202  xdp43lem  1203  xdp45  1204  xdp43  1205  3dp43  1206  oadp35lemc  1209  testmod  1211