Axiom ax-wom 347

Description: 2-variable WOML rule.

Hypothesis

Ref	Expression
ax-wom.1	(a' v (a ^ b)) = 1

Assertion

Ref	Expression
ax-wom	(b v (a' ^ b')) = 1

Detailed syntax breakdown of Axiom ax-wom

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

This axiom is referenced by:  2vwomr2 348  2vwomr1a 349  2vwomlem 351

Copyright terms: Public domain