Axiom ax-wom 343

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 9	. 2 term 1
8	6, 7	wb 1	1 wff (b v (a_|_ ^ b_|_)) = 1

This axiom is referenced by:  2vwomr2 344  2vwomr1a 345  2vwomlem 347

metamath.org