Axiom ax-a4 33

Description: Axiom for ortholattices.

Assertion

Ref	Expression
ax-a4	(a v (b v b')) = (b v b')

Detailed syntax breakdown of Axiom ax-a4

Step	Hyp	Ref	Expression
1		wva	. . 3 term a
2		wvb	. . . 4 term b
3	2	wn 4	. . . 4 term b'
4	2, 3	wo 6	. . 3 term (b v b')
5	1, 4	wo 6	. 2 term (a v (b v b'))
6	5, 4	wb 1	1 wff (a v (b v b')) = (b v b')

This axiom is referenced by:  tt 60  or1 98  wa4 188  lem4.6.6i1j3 1077  com3iia 1085

Copyright terms: Public domain