Theorem 3oa3 1005

Description: 3-variable orthoarguesion law expressed with the 3OA identity abbreviation.

Assertion

Ref	Expression
3oa3	((a ->1 c) ^ (a == c ==OA b)) =< (b ->1 c)

Proof of Theorem 3oa3

Step	Hyp	Ref	Expression
1		df-id3oa 56	. . 3 (a == c ==OA b) = (((a ->1 c) ^ (b ->1 c)) v ((a_|_ ->1 c) ^ (b_|_ ->1 c)))
2	1	lan 70	. 2 ((a ->1 c) ^ (a == c ==OA b)) = ((a ->1 c) ^ (((a ->1 c) ^ (b ->1 c)) v ((a_|_ ->1 c) ^ (b_|_ ->1 c))))
3		3oa2 1004	. 2 ((a ->1 c) ^ (((a ->1 c) ^ (b ->1 c)) v ((a_|_ ->1 c) ^ (b_|_ ->1 c)))) =< (b ->1 c)
4	2, 3	bltr 130	1 ((a ->1 c) ^ (a == c ==OA b)) =< (b ->1 c)

Syntax hints:   =< wle 2  _|_wn 4   v wo 6   ^ wa 7   ->1 wi1 13   == wid3oa 26

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-3oa 978

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

metamath.org