Theorem 2vwomr2 362

Description: 2-variable WOML rule.

Hypothesis

Ref	Expression
2vwomr2.1	(b ∪ (a⊥ ∩ b⊥ )) = 1

Assertion

Ref	Expression
2vwomr2	(a⊥ ∪ (a ∩ b)) = 1

Proof of Theorem 2vwomr2

Step	Hyp	Ref	Expression
1		ancom 74	. . . 4 (a ∩ b) = (b ∩ a)
2		ax-a1 30	. . . . 5 b = b⊥ ⊥
3		ax-a1 30	. . . . 5 a = a⊥ ⊥
4	2, 3	2an 79	. . . 4 (b ∩ a) = (b⊥ ⊥ ∩ a⊥ ⊥ )
5	1, 4	ax-r2 36	. . 3 (a ∩ b) = (b⊥ ⊥ ∩ a⊥ ⊥ )
6	5	lor 70	. 2 (a⊥ ∪ (a ∩ b)) = (a⊥ ∪ (b⊥ ⊥ ∩ a⊥ ⊥ ))
7		ancom 74	. . . . . 6 (a⊥ ∩ b⊥ ) = (b⊥ ∩ a⊥ )
8	2, 7	2or 72	. . . . 5 (b ∪ (a⊥ ∩ b⊥ )) = (b⊥ ⊥ ∪ (b⊥ ∩ a⊥ ))
9	8	ax-r1 35	. . . 4 (b⊥ ⊥ ∪ (b⊥ ∩ a⊥ )) = (b ∪ (a⊥ ∩ b⊥ ))
10		2vwomr2.1	. . . 4 (b ∪ (a⊥ ∩ b⊥ )) = 1
11	9, 10	ax-r2 36	. . 3 (b⊥ ⊥ ∪ (b⊥ ∩ a⊥ )) = 1
12	11	ax-wom 361	. 2 (a⊥ ∪ (b⊥ ⊥ ∩ a⊥ ⊥ )) = 1
13	6, 12	ax-r2 36	1 (a⊥ ∪ (a ∩ b)) = 1

Syntax hints:   = wb 1  ^⊥ wn 4   ∪ wo 6   ∩ wa 7  1wt 8

This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38  ax-wom 361

This theorem depends on definitions:  df-a 40

This theorem is referenced by:  2vwomr2a  364  2vwomlem  365