Theorem 4oa 1018

Description: Variant of proper 4-OA.

Hypotheses

Ref	Expression
4oa.1	e = (((a ^ c) v ((a ->1 d) ^ (c ->1 d))) ^ ((b ^ c) v ((b ->1 d) ^ (c ->1 d))))
4oa.2	f = (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v e)

Assertion

Ref	Expression
4oa	((a ->1 d) ^ f) =< (b ->1 d)

Proof of Theorem 4oa

Step	Hyp	Ref	Expression
1		4oa.2	. . 3 f = (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v e)
2	1	lan 70	. 2 ((a ->1 d) ^ f) = ((a ->1 d) ^ (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v e))
3		axoa4a 1016	. . . 4 (((b_|__|_ ->1 d) ->1 d) ^ ((b_|__|_ ->1 d) v ((a_|__|_ ->1 d) ^ ((((b_|__|_ ->1 d) ^ (a_|__|_ ->1 d)) v (((b_|__|_ ->1 d) ->1 d) ^ ((a_|__|_ ->1 d) ->1 d))) v ((((b_|__|_ ->1 d) ^ (c_|__|_ ->1 d)) v (((b_|__|_ ->1 d) ->1 d) ^ ((c_|__|_ ->1 d) ->1 d))) ^ (((a_|__|_ ->1 d) ^ (c_|__|_ ->1 d)) v (((a_|__|_ ->1 d) ->1 d) ^ ((c_|__|_ ->1 d) ->1 d)))))))) =< ((((b_|__|_ ->1 d) ^ d) v ((a_|__|_ ->1 d) ^ d)) v ((c_|__|_ ->1 d) ^ d))
4		id 58	. . . 4 (b_|__|_ ->1 d) = (b_|__|_ ->1 d)
5		id 58	. . . 4 (a_|__|_ ->1 d) = (a_|__|_ ->1 d)
6		id 58	. . . 4 (c_|__|_ ->1 d) = (c_|__|_ ->1 d)
7	3, 4, 5, 6	oa4to4u2 954	. . 3 ((b_|_ ->1 d) ^ ((b_|__|_ ->1 d) v ((a_|__|_ ->1 d) ^ ((((b_|_ ->1 d) ^ (a_|_ ->1 d)) v ((b_|__|_ ->1 d) ^ (a_|__|_ ->1 d))) v ((((b_|_ ->1 d) ^ (c_|_ ->1 d)) v ((b_|__|_ ->1 d) ^ (c_|__|_ ->1 d))) ^ (((a_|_ ->1 d) ^ (c_|_ ->1 d)) v ((a_|__|_ ->1 d) ^ (c_|__|_ ->1 d)))))))) =< d
8		4oa.1	. . 3 e = (((a ^ c) v ((a ->1 d) ^ (c ->1 d))) ^ ((b ^ c) v ((b ->1 d) ^ (c ->1 d))))
9	7, 8	oa4uto4g 955	. 2 ((a ->1 d) ^ (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v e)) =< (b ->1 d)
10	2, 9	bltr 130	1 ((a ->1 d) ^ f) =< (b ->1 d)

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

This theorem is referenced by:  4oaiii 1019

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-4oa 1012

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

metamath.org