Theorem 2vwomr2 344

Description: 2-variable WOML rule.

Hypothesis

Ref	Expression
2vwomr2.1	(b v (a_|_ ^ b_|_)) = 1

Assertion

Ref	Expression
2vwomr2	(a_|_ v (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_|_ v (a ^ b)) = (a_|_ v (b_|__|_ ^ a_|__|_))
7		ancom 68	. . . . . 6 (a_|_ ^ b_|_) = (b_|_ ^ a_|_)
8	2, 7	2or 67	. . . . 5 (b v (a_|_ ^ b_|_)) = (b_|__|_ v (b_|_ ^ a_|_))
9	8	ax-r1 34	. . . 4 (b_|__|_ v (b_|_ ^ a_|_)) = (b v (a_|_ ^ b_|_))
10		2vwomr2.1	. . . 4 (b v (a_|_ ^ b_|_)) = 1
11	9, 10	ax-r2 35	. . 3 (b_|__|_ v (b_|_ ^ a_|_)) = 1
12	11	ax-wom 343	. 2 (a_|_ v (b_|__|_ ^ a_|__|_)) = 1
13	6, 12	ax-r2 35	1 (a_|_ v (a ^ b)) = 1

Syntax hints:   = wb 1  _|_wn 4   v 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