Theorem tr 62

Description: Transitive inference rule for ortholattices.

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 is referenced by:  k1-7 354  k1-8a 355  k1-8b 356  k1-2 357  k1-3 358  k1-4 359  k1-5 360

This theorem was proved from axioms:  ax-r2 36

Copyright terms: Public domain