Axiom ax-a5 34

Description: Axiom for ortholattices.

Assertion

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

Detailed syntax breakdown of Axiom ax-a5

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

This axiom is referenced by:  or0 96  oridm 104  a5b 114  a5c 115  wa5 189

Copyright terms: Public domain