Theorem oa43v 1008

Description: Derivation of 3-variable OA from 4-variable OA.

Assertion

Ref	Expression
oa43v	((a ->2 b) ^ ((b v c)_|_ v ((a ->2 b) ^ (a ->2 c)))) =< (a ->2 c)

Proof of Theorem oa43v

Step	Hyp	Ref	Expression
1		ud2lem0c 270	. . . . 5 (a ->2 c)_|_ = (c_|_ ^ (a v c))
2		lea 152	. . . . 5 (c_|_ ^ (a v c)) =< c_|_
3	1, 2	bltr 130	. . . 4 (a ->2 c)_|_ =< c_|_
4		ud2lem0c 270	. . . . 5 (a ->2 b)_|_ = (b_|_ ^ (a v b))
5		lea 152	. . . . 5 (b_|_ ^ (a v b)) =< b_|_
6	4, 5	bltr 130	. . . 4 (a ->2 b)_|_ =< b_|_
7	3, 6	ax-oal4 1006	. . . 4 (((a ->2 c)_|_ v c) ^ ((a ->2 b)_|_ v b)) =< (c v ((a ->2 c)_|_ ^ ((a ->2 b)_|_ v (((a ->2 c)_|_ v (a ->2 b)_|_) ^ (c v b)))))
8		id 58	. . . 4 (a ->2 c)_|_ = (a ->2 c)_|_
9		id 58	. . . 4 (a ->2 b)_|_ = (a ->2 b)_|_
10	3, 6, 7, 8, 9	oa4v3v 914	. . 3 (c_|_ ^ ((a ->2 c) v ((a ->2 b) ^ ((c v b)_|_ v ((a ->2 c) ^ (a ->2 b)))))) =< ((c_|_ ^ (a ->2 c)) v (b_|_ ^ (a ->2 b)))
11	10	oal42 915	. 2 (c_|_ ^ ((a ->2 c) v ((a ->2 b) ^ ((c v b)_|_ v ((a ->2 c) ^ (a ->2 b)))))) =< a_|_
12	11	oa23 916	1 ((a ->2 b) ^ ((b v c)_|_ v ((a ->2 b) ^ (a ->2 c)))) =< (a ->2 c)

Syntax hints:   =< wle 2  _|_wn 4   v wo 6   ^ wa 7   ->2 wi2 14

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

This theorem depends on definitions:  df-b 38  df-a 39  df-t 40  df-f 41  df-i2 44  df-le1 122  df-le2 123  df-c1 124  df-c2 125

metamath.org