Theorem d6oa 977

Description: Derivation of 6-variable orthoarguesian law from OA distributive law.

Hypotheses

Ref	Expression
d6oa.1	a =< b_|_
d6oa.2	c =< d_|_
d6oa.3	e =< f_|_

Assertion

Ref	Expression
d6oa	(((a v b) ^ (c v d)) ^ (e v f)) =< (b v (a ^ (c v (((a v c) ^ (b v d)) ^ (((a v e) ^ (b v f)) v ((c v e) ^ (d v f)))))))

Proof of Theorem d6oa

Step	Hyp	Ref	Expression
1		d6oa.1	. 2 a =< b_|_
2		d6oa.2	. 2 c =< d_|_
3		d6oa.3	. 2 e =< f_|_
4		id 58	. 2 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_)) = (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))
5		id 58	. 2 a_|_ = a_|_
6		id 58	. 2 c_|_ = c_|_
7		id 58	. 2 e_|_ = e_|_
8		id 58	. . . . 5 (((c_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ^ (a_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_)))) v (((c_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ^ ((a_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))))) = (((c_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ^ (a_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_)))) v (((c_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ^ ((a_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_)))))
9		id 58	. . . . 5 ((((c_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ^ (e_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_)))) v (((c_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ^ ((e_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))))) ^ (((a_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ^ (e_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_)))) v (((a_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ^ ((e_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_)))))) = ((((c_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ^ (e_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_)))) v (((c_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ^ ((e_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))))) ^ (((a_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ^ (e_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_)))) v (((a_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ^ ((e_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))))))
10	8, 9	d4oa 976	. . . 4 (((c_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ^ ((((c_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ^ (a_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_)))) v (((c_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ^ ((a_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))))) v ((((c_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ^ (e_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_)))) v (((c_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ^ ((e_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))))) ^ (((a_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ^ (e_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_)))) v (((a_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ^ ((e_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_)))))))) =< ((a_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_)))
11		id 58	. . . 4 (a_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) = (a_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_)))
12		id 58	. . . 4 (c_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) = (c_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_)))
13		id 58	. . . 4 (e_|_ ->1 (((a_|_ ^ b_|_) v (c