Theorem 2vwomr2 344

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 68	. . . 4 (a ∩ b) = (b ∩ a)
2		ax-a1 29	. . . . 5 b = b⊥ ⊥
3		ax-a1 29	. . . . 5 a = a⊥ ⊥
4	2, 3	2an 72	. . . 4 (b ∩ a) = (b⊥ ⊥ ∩ a⊥ ⊥ )
5	1, 4	ax-r2 35	. . 3 (a ∩ b) = (b⊥ ⊥ ∩ a⊥ ⊥ )
6	5	lor 66	. 2 (a⊥ ∪ (a ∩ b)) = (a⊥ ∪ (b⊥ ⊥ ∩ a⊥ ⊥ ))
7		ancom 68	. . . . . 6 (a⊥ ∩ b⊥ ) = (b⊥ ∩ a⊥ )
8	2, 7	2or 67	. . . . 5 (b ∪ (a⊥ ∩ b⊥ )) = (b⊥ ⊥ ∪ (b⊥ ∩ a⊥ ))
9	8	ax-r1 34	. . . 4 (b⊥ ⊥ ∪ (b⊥ ∩ a⊥ )) = (b ∪ (a⊥ ∩ b⊥ ))
10		2vwomr2.1	. . . 4 (b ∪ (a⊥ ∩ b⊥ )) = 1
11	9, 10	ax-r2 35	. . 3 (b⊥ ⊥ ∪ (b⊥ ∩ a⊥ )) = 1
12	11	ax-wom 343	. 2 (a⊥ ∪ (b⊥ ⊥ ∩ a⊥ ⊥ )) = 1
13	6, 12	ax-r2 35	1 (a⊥ ∪ (a ∩ b)) = 1

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

This theorem is referenced by:  2vwomr2a 346  2vwomlem 347

This theorem was proved from axioms:  ax-a1 29  ax-a2 30  ax-r1 34  ax-r2 35  ax-r4 36  ax-r5 37  ax-wom 343

This theorem depends on definitions:  df-a 39

metamath.org