Axiom ax-wom 343

Description: 2-variable WOML rule.

Hypothesis

Ref	Expression
ax-wom.1	(a⊥ ∪ (a ∩ b)) = 1

Assertion

Ref	Expression
ax-wom	(b ∪ (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 ∪ (a⊥ ∩ b⊥ ))
7		wt 9	. 2 term  1
8	6, 7	wb 1	1 wff  (b ∪ (a⊥ ∩ b⊥ )) = 1

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

metamath.org