Theorem oal2 979

Description: Orthoarguesian law - ->2 version.

Assertion

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

Proof of Theorem oal2

Step	Hyp	Ref	Expression
1		ax-3oa 978	. 2 ((b_|_ ->1 a_|_) ^ ((b_|_ ^ c_|_) v ((b_|_ ->1 a_|_) ^ (c_|_ ->1 a_|_)))) =< (c_|_ ->1 a_|_)
2		i2i1 259	. . 3 (a ->2 b) = (b_|_ ->1 a_|_)
3		anor3 82	. . . . 5 (b_|_ ^ c_|_) = (b v c)_|_
4	3	ax-r1 34	. . . 4 (b v c)_|_ = (b_|_ ^ c_|_)
5		i2i1 259	. . . . 5 (a ->2 c) = (c_|_ ->1 a_|_)
6	2, 5	2an 72	. . . 4 ((a ->2 b) ^ (a ->2 c)) = ((b_|_ ->1 a_|_) ^ (c_|_ ->1 a_|_))
7	4, 6	2or 67	. . 3 ((b v c)_|_ v ((a ->2 b) ^ (a ->2 c))) = ((b_|_ ^ c_|_) v ((b_|_ ->1 a_|_) ^ (c_|_ ->1 a_|_)))
8	2, 7	2an 72	. 2 ((a ->2 b) ^ ((b v c)_|_ v ((a ->2 b) ^ (a ->2 c)))) = ((b_|_ ->1 a_|_) ^ ((b_|_ ^ c_|_) v ((b_|_ ->1 a_|_) ^ (c_|_ ->1 a_|_))))
9	1, 8, 5	le3tr1 132	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   ->1 wi1 13   ->2 wi2 14

This theorem is referenced by:  oal1 980  oaliii 981  oagen2 996  mloa 998  oadistc0 1001

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

This theorem depends on definitions:  df-a 39  df-i1 43  df-i2 44  df-le1 122  df-le2 123

metamath.org