Theorem wql2lem2 281

Description: Lemma for ->2 WQL axiom.

Hypothesis

Ref	Expression
wql2lem2.1	((a v c) ->2 (b v c)) = 1

Assertion

Ref	Expression
wql2lem2	((a v (b v c))_|_ v (b v c)) = 1

Proof of Theorem wql2lem2

Step	Hyp	Ref	Expression
1		df-i2 44	. . . 4 ((a v c) ->2 (b v c)) = ((b v c) v ((a v c)_|_ ^ (b v c)_|_))
2		anor3 82	. . . . . 6 ((a v c)_|_ ^ (b v c)_|_) = ((a v c) v (b v c))_|_
3		ax-a3 31	. . . . . . . . . 10 ((a v b) v c) = (a v (b v c))
4	3	ax-r1 34	. . . . . . . . 9 (a v (b v c)) = ((a v b) v c)
5		orordir 105	. . . . . . . . 9 ((a v b) v c) = ((a v c) v (b v c))
6	4, 5	ax-r2 35	. . . . . . . 8 (a v (b v c)) = ((a v c) v (b v c))
7	6	ax-r4 36	. . . . . . 7 (a v (b v c))_|_ = ((a v c) v (b v c))_|_
8	7	ax-r1 34	. . . . . 6 ((a v c) v (b v c))_|_ = (a v (b v c))_|_
9	2, 8	ax-r2 35	. . . . 5 ((a v c)_|_ ^ (b v c)_|_) = (a v (b v c))_|_
10	9	lor 66	. . . 4 ((b v c) v ((a v c)_|_ ^ (b v c)_|_)) = ((b v c) v (a v (b v c))_|_)
11		ax-a2 30	. . . 4 ((b v c) v (a v (b v c))_|_) = ((a v (b v c))_|_ v (b v c))
12	1, 10, 11	3tr 62	. . 3 ((a v c) ->2 (b v c)) = ((a v (b v c))_|_ v (b v c))
13	12	ax-r1 34	. 2 ((a v (b v c))_|_ v (b v c)) = ((a v c) ->2 (b v c))
14		wql2lem2.1	. 2 ((a v c) ->2 (b v c)) = 1
15	13, 14	ax-r2 35	1 ((a v (b v c))_|_ v (b v c)) = 1

Syntax hints:   = wb 1  _|_wn 4   v wo 6   ^ wa 7  1wt 9   ->2 wi2 14

This theorem is referenced by:  wql2lem4 283

This theorem was proved from axioms:  ax-a1 29  ax-a2 30  ax-a3 31  ax-a5 33  ax-r1 34  ax-r2 35  ax-r4 36  ax-r5 37

This theorem depends on definitions:  df-a 39  df-t 40  df-f 41  df-i2 44

metamath.org