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  1124  vneulem2  1132  vneulem3  1133  vneulem6  1136  vneulem7  1137  vneulem8  1138  vneulem10  1140  vneulem11  1141  vneulem12  1142  vneulem13  1143  vneulem14  1144  vneulem16  1146  vneulem  1147  vneulemexp  1148  l42modlem1  1149  modexp  1152  dp15lema  1154  dp15leme  1158  dp15lemg  1160  dp53lema  1163  dp53lemb  1164  dp53lemd  1166  dp53leme  1167  dp53lemf  1168  dp35leme  1173  dp35lemb  1176  dp35lembb  1177  dp35lem0  1179  dp41lema  1182  dp41lemb  1183  dp41lemc0  1184  dp41leme  1187  dp41lemf  1188  dp41lemg  1189  dp41lemj  1191  dp41lemk  1192  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  testmod  1213  testmod1  1214  testmod2  1215  testmod2expanded  1216  testmod3  1217