Theorem tr 62

Description: Transitive inference rule for ortholattices. (Contributed by NM, 26-May-2008.)

Hypotheses

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

Assertion

Ref	Expression
tr	a = c

Proof of Theorem tr

Step	Hyp	Ref	Expression
1		tr.1	. 2 a = b
2		tr.2	. 2 b = c
3	1, 2	ax-r2 36	1 a = c

Syntax hints:   = wb 1

This theorem was proved from axioms:  ax-r2 36

This theorem is referenced by:  k1-7  354  k1-8a  355  k1-8b  356  k1-2  357  k1-3  358  k1-4  359  k1-5  360  oa3moa3  1029  mldual  1122  vneulem2  1130  vneulem3  1131  vneulem6  1134  vneulem7  1135  vneulem8  1136  vneulem10  1138  vneulem11  1139  vneulem12  1140  vneulem13  1141  vneulem14  1142  vneulem16  1144  vneulem  1145  vneulemexp  1146  l42modlem1  1147  modexp  1150  dp15lema  1152  dp15leme  1156  dp15lemg  1158  dp53lema  1161  dp53lemb  1162  dp53lemd  1164  dp53leme  1165  dp53lemf  1166  dp35leme  1171  dp35lemb  1174  dp35lembb  1175  dp35lem0  1177  dp41lema  1180  dp41lemb  1181  dp41lemc0  1182  dp41leme  1185  dp41lemf  1186  dp41lemg  1187  dp41lemj  1189  dp41lemk  1190  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  testmod  1211  testmod1  1212  testmod2  1213  testmod2expanded  1214  testmod3  1215