Theorem 4oagen1b 1022

Description: "Generalized" 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)
4oagen1b.1	g =< f
4oagen1b.2	h =< (a ->1 d)

Assertion

Ref	Expression
4oagen1b	(h ^ (g v ((a ->1 d) ^ (b ->1 d)))) = (h ^ (b ->1 d))

Proof of Theorem 4oagen1b

Step	Hyp	Ref	Expression
1		4oa.1	. . . 4 e = (((a ^ c) v ((a ->1 d) ^ (c ->1 d))) ^ ((b ^ c) v ((b ->1 d) ^ (c ->1 d))))
2		4oa.2	. . . 4 f = (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v e)
3		4oagen1b.1	. . . 4 g =< f
4	1, 2, 3	4oagen1 1021	. . 3 ((a ->1 d) ^ (g v ((a ->1 d) ^ (b ->1 d)))) = ((a ->1 d) ^ (b ->1 d))
5	4	lan 70	. 2 (h ^ ((a ->1 d) ^ (g v ((a ->1 d) ^ (b ->1 d))))) = (h ^ ((a ->1 d) ^ (b ->1 d)))
6		anass 69	. . . 4 ((h ^ (a ->1 d)) ^ (g v ((a ->1 d) ^ (b ->1 d)))) = (h ^ ((a ->1 d) ^ (g v ((a ->1 d) ^ (b ->1 d)))))
7	6	ax-r1 34	. . 3 (h ^ ((a ->1 d) ^ (g v ((a ->1 d) ^ (b ->1 d))))) = ((h ^ (a ->1 d)) ^ (g v ((a ->1 d) ^ (b ->1 d))))
8		4oagen1b.2	. . . . 5 h =< (a ->1 d)
9	8	df2le2 128	. . . 4 (h ^ (a ->1 d)) = h
10	9	ran 71	. . 3 ((h ^ (a ->1 d)) ^ (g v ((a ->1 d) ^ (b ->1 d)))) = (h ^ (g v ((a ->1 d) ^ (b ->1 d))))
11	7, 10	ax-r2 35	. 2 (h ^ ((a ->1 d) ^ (g v ((a ->1 d) ^ (b ->1 d))))) = (h ^ (g v ((a ->1 d) ^ (b ->1 d))))
12		anass 69	. . . 4 ((h ^ (a ->1 d)) ^ (b ->1 d)) = (h ^ ((a ->1 d) ^ (b ->1 d)))
13	12	ax-r1 34	. . 3 (h ^ ((a ->1 d) ^ (b ->1 d))) = ((h ^ (a ->1 d)) ^ (b ->1 d))
14	9	ran 71	. . 3 ((h ^ (a ->1 d)) ^ (b ->1 d)) = (h ^ (b ->1 d))
15	13, 14	ax-r2 35	. 2 (h ^ ((a ->1 d) ^ (b ->1 d))) = (h ^ (b ->1 d))
16	5, 11, 15	3tr2 61	1 (h ^ (g v ((a ->1 d) ^ (b ->1 d)))) = (h ^ (b ->1 d))

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

This theorem is referenced by:  4oadist 1023

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