QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  xdp43lem Structured version   Unicode version

Theorem xdp43lem 1203
Description: Part of proof (4)=>(3) in Day/Pickering 1982.
Hypotheses
Ref Expression
xxdp.1 p2 =< (a2 v b2)
xxdp.c0 c0 = ((a1 v a2) ^ (b1 v b2))
xxdp.c1 c1 = ((a0 v a2) ^ (b0 v b2))
xxdp.c2 c2 = ((a0 v a1) ^ (b0 v b1))
xxdp.d d = (a2 v (a0 ^ (a1 v b1)))
xxdp.e e = (b0 ^ (a0 v p0))
xxdp.p p = (((a0 v b0) ^ (a1 v b1)) ^ (a2 v b2))
xxdp.p0 p0 = ((a1 v b1) ^ (a2 v b2))
xxdp.p2 p2 = ((a0 v b0) ^ (a1 v b1))
Assertion
Ref Expression
xdp43lem p =< (a0 v (b0 ^ (b1 v (c2 ^ (c0 v c1)))))

Proof of Theorem xdp43lem
StepHypRef Expression
1 leor 159 . 2 p =< (a0 v p)
2 leo 158 . . 3 a0 =< (a0 v (b0 ^ (b1 v (c2 ^ (c0 v c1)))))
3 xxdp.p . . . . . . . 8 p = (((a0 v b0) ^ (a1 v b1)) ^ (a2 v b2))
4 anass 76 . . . . . . . 8 (((a0 v b0) ^ (a1 v b1)) ^ (a2 v b2)) = ((a0 v b0) ^ ((a1 v b1) ^ (a2 v b2)))
53, 4tr 62 . . . . . . 7 p = ((a0 v b0) ^ ((a1 v b1) ^ (a2 v b2)))
6 xxdp.p0 . . . . . . . . . . 11 p0 = ((a1 v b1) ^ (a2 v b2))
76lan 77 . . . . . . . . . 10 ((a0 v b0) ^ p0) = ((a0 v b0) ^ ((a1 v b1) ^ (a2 v b2)))
87cm 61 . . . . . . . . 9 ((a0 v b0) ^ ((a1 v b1) ^ (a2 v b2))) = ((a0 v b0) ^ p0)
9 leao4 165 . . . . . . . . 9 ((a0 v b0) ^ p0) =< (a0 v p0)
108, 9bltr 138 . . . . . . . 8 ((a0 v b0) ^ ((a1 v b1) ^ (a2 v b2))) =< (a0 v p0)
11 lea 160 . . . . . . . . 9 ((a0 v b0) ^ ((a1 v b1) ^ (a2 v b2))) =< (a0 v b0)
12 orcom 73 . . . . . . . . 9 (a0 v b0) = (b0 v a0)
1311, 12lbtr 139 . . . . . . . 8 ((a0 v b0) ^ ((a1 v b1) ^ (a2 v b2))) =< (b0 v a0)
1410, 13ler2an 173 . . . . . . 7 ((a0 v b0) ^ ((a1 v b1) ^ (a2 v b2))) =< ((a0 v p0) ^ (b0 v a0))
155, 14bltr 138 . . . . . 6 p =< ((a0 v p0) ^ (b0 v a0))
16 leo 158 . . . . . . . 8 a0 =< (a0 v p0)
1716mldual2i 1125 . . . . . . 7 ((a0 v p0) ^ (b0 v a0)) = (((a0 v p0) ^ b0) v a0)
18 ancom 74 . . . . . . . 8 ((a0 v p0) ^ b0) = (b0 ^ (a0 v p0))
1918ror 71 . . . . . . 7 (((a0 v p0) ^ b0) v a0) = ((b0 ^ (a0 v p0)) v a0)
2017, 19tr 62 . . . . . 6 ((a0 v p0) ^ (b0 v a0)) = ((b0 ^ (a0 v p0)) v a0)
2115, 20lbtr 139 . . . . 5 p =< ((b0 ^ (a0 v p0)) v a0)
222lelor 166 . . . . 5 ((b0 ^ (a0 v p0)) v a0) =< ((b0 ^ (a0 v p0)) v (a0 v (b0 ^ (b1 v (c2 ^ (c0 v c1))))))
2321, 22letr 137 . . . 4 p =< ((b0 ^ (a0 v p0)) v (a0 v (b0 ^ (b1 v (c2 ^ (c0 v c1))))))
24 lea 160 . . . . . . . 8 (b0 ^ (a0 v p0)) =< b0
25 leor 159 . . . . . . . . 9 (b0 ^ (a0 v p0)) =< (b1 v (b0 ^ (a0 v p0)))
26 leo 158 . . . . . . . . . 10 b1 =< (b1 v ((a0 v a1) ^ (c0 v c1)))
27 leo 158 . . . . . . . . . . . . . 14 (b0 ^ (a0 v p0)) =< ((b0 ^ (a0 v p0)) v b1)
286lor 70 . . . . . . . . . . . . . . . 16 (a0 v p0) = (a0 v ((a1 v b1) ^ (a2 v b2)))
2928lan 77 . . . . . . . . . . . . . . 15 (b0 ^ (a0 v p0)) = (b0 ^ (a0 v ((a1 v b1) ^ (a2 v b2))))
30 lear 161 . . . . . . . . . . . . . . . 16 (b0 ^ (a0 v ((a1 v b1) ^ (a2 v b2)))) =< (a0 v ((a1 v b1) ^ (a2 v b2)))
31 lea 160 . . . . . . . . . . . . . . . . . 18 ((a1 v b1) ^ (a2 v b2)) =< (a1 v b1)
3231lelor 166 . . . . . . . . . . . . . . . . 17 (a0 v ((a1 v b1) ^ (a2 v b2))) =< (a0 v (a1 v b1))
33 ax-a3 32 . . . . . . . . . . . . . . . . . 18 ((a0 v a1) v b1) = (a0 v (a1 v b1))
3433cm 61 . . . . . . . . . . . . . . . . 17 (a0 v (a1 v b1)) = ((a0 v a1) v b1)
3532, 34lbtr 139 . . . . . . . . . . . . . . . 16 (a0 v ((a1 v b1) ^ (a2 v b2))) =< ((a0 v a1) v b1)
3630, 35letr 137 . . . . . . . . . . . . . . 15 (b0 ^ (a0 v ((a1 v b1) ^ (a2 v b2)))) =< ((a0 v a1) v b1)
3729, 36bltr 138 . . . . . . . . . . . . . 14 (b0 ^ (a0 v p0)) =< ((a0 v a1) v b1)
3827, 37ler2an 173 . . . . . . . . . . . . 13 (b0 ^ (a0 v p0)) =< (((b0 ^ (a0 v p0)) v b1) ^ ((a0 v a1) v b1))
39 leor 159 . . . . . . . . . . . . . . 15 b1 =< ((b0 ^ (a0 v p0)) v b1)
4039mldual2i 1125 . . . . . . . . . . . . . 14 (((b0 ^ (a0 v p0)) v b1) ^ ((a0 v a1) v b1)) = ((((b0 ^ (a0 v p0)) v b1) ^ (a0 v a1)) v b1)
41 ancom 74 . . . . . . . . . . . . . . 15 (((b0 ^ (a0 v p0)) v b1) ^ (a0 v a1)) = ((a0 v a1) ^ ((b0 ^ (a0 v p0)) v b1))
4241ror 71 . . . . . . . . . . . . . 14 ((((b0 ^ (a0 v p0)) v b1) ^ (a0 v a1)) v b1) = (((a0 v a1) ^ ((b0 ^ (a0 v p0)) v b1)) v b1)
4340, 42tr 62 . . . . . . . . . . . . 13 (((b0 ^ (a0 v p0)) v b1) ^ ((a0 v a1) v b1)) = (((a0 v a1) ^ ((b0 ^ (a0 v p0)) v b1)) v b1)
4438, 43lbtr 139 . . . . . . . . . . . 12 (b0 ^ (a0 v p0)) =< (((a0 v a1) ^ ((b0 ^ (a0 v p0)) v b1)) v b1)
4526lelor 166 . . . . . . . . . . . 12 (((a0 v a1) ^ ((b0 ^ (a0 v p0)) v b1)) v b1) =< (((a0 v a1) ^ ((b0 ^ (a0 v p0)) v b1)) v (b1 v ((a0 v a1) ^ (c0 v c1))))
4644, 45letr 137 . . . . . . . . . . 11 (b0 ^ (a0 v p0)) =< (((a0 v a1) ^ ((b0 ^ (a0 v p0)) v b1)) v (b1 v ((a0 v a1) ^ (c0 v c1))))
47 lea 160 . . . . . . . . . . . . . . . 16 ((a0 v a1) ^ ((b0 ^ (a0 v p0)) v b1)) =< (a0 v a1)
48 ax-a2 31 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (a0 v a1) = (a1 v a0)
49 ax-a2 31 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (e v b1) = (b1 v e)
5048, 492an 79 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((a0 v a1) ^ (e v b1)) = ((a1 v a0) ^ (b1 v e))
51 ancom 74 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((a1 v a0) ^ (b1 v e)) = ((b1 v e) ^ (a1 v a0))
5250, 51tr 62 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((a0 v a1) ^ (e v b1)) = ((b1 v e) ^ (a1 v a0))
53 leor 159 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 b1 =< (a1 v b1)
5453leror 152 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (b1 v e) =< ((a1 v b1) v e)
55 leo 158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (a1 v a0) =< ((a1 v a0) v e)
5654, 55le2an 169 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((b1 v e) ^ (a1 v a0)) =< (((a1 v b1) v e) ^ ((a1 v a0) v e))
5752, 56bltr 138 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((a0 v a1) ^ (e v b1)) =< (((a1 v b1) v e) ^ ((a1 v a0) v e))
5857df2le2 136 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((a0 v a1) ^ (e v b1)) ^ (((a1 v b1) v e) ^ ((a1 v a0) v e))) = ((a0 v a1) ^ (e v b1))
5958cm 61 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((a0 v a1) ^ (e v b1)) = (((a0 v a1) ^ (e v b1)) ^ (((a1 v b1) v e) ^ ((a1 v a0) v e)))
60 anass 76 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((a0 v a1) ^ (e v b1)) ^ ((a1 v b1) v e)) ^ ((a1 v a0) v e)) = (((a0 v a1) ^ (e v b1)) ^ (((a1 v b1) v e) ^ ((a1 v a0) v e)))
6160cm 61 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((a0 v a1) ^ (e v b1)) ^ (((a1 v b1) v e) ^ ((a1 v a0) v e))) = ((((a0 v a1) ^ (e v b1)) ^ ((a1 v b1) v e)) ^ ((a1 v a0) v e))
6259, 61tr 62 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((a0 v a1) ^ (e v b1)) = ((((a0 v a1) ^ (e v b1)) ^ ((a1 v b1) v e)) ^ ((a1 v a0) v e))
63 ax-a2 31 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (a1 v a0) = (a0 v a1)
6463ror 71 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((a1 v a0) v e) = ((a0 v a1) v e)
65 or32 82 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((a0 v a1) v e) = ((a0 v e) v a1)
6664, 65tr 62 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((a1 v a0) v e) = ((a0 v e) v a1)
6766lan 77 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((a1 v b1) v e) ^ ((a1 v a0) v e)) = (((a1 v b1) v e) ^ ((a0 v e) v a1))
68 ancom 74 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((a1 v b1) v e) ^ ((a0 v e) v a1)) = (((a0 v e) v a1) ^ ((a1 v b1) v e))
6967, 68tr 62 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((a1 v b1) v e) ^ ((a1 v a0) v e)) = (((a0 v e) v a1) ^ ((a1 v b1) v e))
70 leor 159 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 e =< (a0 v e)
7170ler 149 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 e =< ((a0 v e) v a1)
7271mldual2i 1125 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((a0 v e) v a1) ^ ((a1 v b1) v e)) = ((((a0 v e) v a1) ^ (a1 v b1)) v e)
73 ancom 74 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((a0 v e) v a1) ^ (a1 v b1)) = ((a1 v b1) ^ ((a0 v e) v a1))
74 leo 158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 a1 =< (a1 v b1)
7574mldual2i 1125 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((a1 v b1) ^ ((a0 v e) v a1)) = (((a1 v b1) ^ (a0 v e)) v a1)
7673, 75tr 62 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((a0 v e) v a1) ^ (a1 v b1)) = (((a1 v b1) ^ (a0 v e)) v a1)
7776ror 71 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((a0 v e) v a1) ^ (a1 v b1)) v e) = ((((a1 v b1) ^ (a0 v e)) v a1) v e)
7869, 72, 773tr 65 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((a1 v b1) v e) ^ ((a1 v a0) v e)) = ((((a1 v b1) ^ (a0 v e)) v a1) v e)
79 orass 75 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((a1 v b1) ^ (a0 v e)) v a1) v e) = (((a1 v b1) ^ (a0 v e)) v (a1 v e))
80 orcom 73 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((a1 v b1) ^ (a0 v e)) v (a1 v e)) = ((a1 v e) v ((a1 v b1) ^ (a0 v e)))
8178, 79, 803tr 65 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((a1 v b1) v e) ^ ((a1 v a0) v e)) = ((a1 v e) v ((a1 v b1) ^ (a0 v e)))
82 leo 158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (a1 v e) =< ((a1 v e) v (((a0 v a1) ^ (e v b1)) ^ (((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2)))))
83 ancom 74 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((a0 v e) ^ (a1 v b1)) = ((a1 v b1) ^ (a0 v e))
8483cm 61 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((a1 v b1) ^ (a0 v e)) = ((a0 v e) ^ (a1 v b1))
85 xxdp.e . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 e = (b0 ^ (a0 v p0))
8685, 29tr 62 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 e = (b0 ^ (a0 v ((a1 v b1) ^ (a2 v b2))))
8786lor 70 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (a0 v e) = (a0 v (b0 ^ (a0 v ((a1 v b1) ^ (a2 v b2)))))
8887ran 78 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((a0 v e) ^ (a1 v b1)) = ((a0 v (b0 ^ (a0 v ((a1 v b1) ^ (a2 v b2))))) ^ (a1 v b1))
89 le1 146 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 b0 =< 1
9089leran 153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (b0 ^ (a0 v ((a1 v b1) ^ (a2 v b2)))) =< (1 ^ (a0 v ((a1 v b1) ^ (a2 v b2))))
9190lelor 166 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (a0 v (b0 ^ (a0 v ((a1 v b1) ^ (a2 v b2))))) =< (a0 v (1 ^ (a0 v ((a1 v b1) ^ (a2 v b2)))))
9291leran 153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((a0 v (b0 ^ (a0 v ((a1 v b1) ^ (a2 v b2))))) ^ (a1 v b1)) =< ((a0 v (1 ^ (a0 v ((a1 v b1) ^ (a2 v b2))))) ^ (a1 v b1))
93 an1r 107 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (1 ^ (a0 v ((a1 v b1) ^ (a2 v b2)))) = (a0 v ((a1 v b1) ^ (a2 v b2)))
9493lor 70 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (a0 v (1 ^ (a0 v ((a1 v b1) ^ (a2 v b2))))) = (a0 v (a0 v ((a1 v b1) ^ (a2 v b2))))
95 orass 75 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((a0 v a0) v ((a1 v b1) ^ (a2 v b2))) = (a0 v (a0 v ((a1 v b1) ^ (a2 v b2))))
9695cm 61 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (a0 v (a0 v ((a1 v b1) ^ (a2 v b2)))) = ((a0 v a0) v ((a1 v b1) ^ (a2 v b2)))
97 oridm 110 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (a0 v a0) = a0
9897ror 71 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((a0 v a0) v ((a1 v b1) ^ (a2 v b2))) = (a0 v ((a1 v b1) ^ (a2 v b2)))
99 orcom 73 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (a0 v ((a1 v b1) ^ (a2 v b2))) = (((a1 v b1) ^ (a2 v b2)) v a0)
10098, 99tr 62 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((a0 v a0) v ((a1 v b1) ^ (a2 v b2))) = (((a1 v b1) ^ (a2 v b2)) v a0)
10194, 96, 1003tr 65 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (a0 v (1 ^ (a0 v ((a1 v b1) ^ (a2 v b2))))) = (((a1 v b1) ^ (a2 v b2)) v a0)
102101ran 78 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((a0 v (1 ^ (a0 v ((a1 v b1) ^ (a2 v b2))))) ^ (a1 v b1)) = ((((a1 v b1) ^ (a2 v b2)) v a0) ^ (a1 v b1))
10331mlduali 1126 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((((a1 v b1) ^ (a2 v b2)) v a0) ^ (a1 v b1)) = (((a1 v b1) ^ (a2 v b2)) v (a0 ^ (a1 v b1)))
104102, 103tr 62 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((a0 v (1 ^ (a0 v ((a1 v b1) ^ (a2 v b2))))) ^ (a1 v b1)) = (((a1 v b1) ^ (a2 v b2)) v (a0 ^ (a1 v b1)))
105 lear 161 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((a1 v b1) ^ (a2 v b2)) =< (a2 v b2)
106105leror 152 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((a1 v b1) ^ (a2 v b2)) v (a0 ^ (a1 v b1))) =< ((a2 v b2) v (a0 ^ (a1 v b1)))
107104, 106bltr 138 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((a0 v (1 ^ (a0 v ((a1 v b1) ^ (a2 v b2))))) ^ (a1 v b1)) =< ((a2 v b2) v (a0 ^ (a1 v b1)))
108 or32 82 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((a2 v b2) v (a0 ^ (a1 v b1))) = ((a2 v (a0 ^ (a1 v b1))) v b2)
109 xxdp.d . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 d = (a2 v (a0 ^ (a1 v b1)))
110109ror 71 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (d v b2) = ((a2 v (a0 ^ (a1 v b1))) v b2)
111110cm 61 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((a2 v (a0 ^ (a1 v b1))) v b2) = (d v b2)
112108, 111tr 62 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((a2 v b2) v (a0 ^ (a1 v b1))) = (d v b2)
113107, 112lbtr 139 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((a0 v (1 ^ (a0 v ((a1 v b1) ^ (a2 v b2))))) ^ (a1 v b1)) =< (d v b2)
11492, 113letr 137 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((a0 v (b0 ^ (a0 v ((a1 v b1) ^ (a2 v b2))))) ^ (a1 v b1)) =< (d v b2)
11588, 114bltr 138 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((a0 v e) ^ (a1 v b1)) =< (d v b2)
11684, 115bltr 138 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((a1 v b1) ^ (a0 v e)) =< (d v b2)
117116df2le2 136 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((a1 v b1) ^ (a0 v e)) ^ (d v b2)) = ((a1 v b1) ^ (a0 v e))
118117cm 61 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((a1 v b1) ^ (a0 v e)) = (((a1 v b1) ^ (a0 v e)) ^ (d v b2))
119 id 59 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((a1 v b1) ^ (a0 v e)) ^ (d v b2)) = (((a1 v b1) ^ (a0 v e)) ^ (d v b2))
120119cm 61 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((a1 v b1) ^ (a0 v e)) ^ (d v b2)) = (((a1 v b1) ^ (a0 v e)) ^ (d v b2))
121118, 120tr 62 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((a1 v b1) ^ (a0 v e)) = (((a1 v b1) ^ (a0 v e)) ^ (d v b2))
122 id 59 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((a0 v d) ^ (e v b2)) = ((a0 v d) ^ (e v b2))
123 id 59 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((a1 v d) ^ (b1 v b2)) = ((a1 v d) ^ (b1 v b2))
124 orcom 73 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (a0 v a1) = (a1 v a0)
125 orcom 73 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (e v b1) = (b1 v e)
126124, 1252an 79 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((a0 v a1) ^ (e v b1)) = ((a1 v a0) ^ (b1 v e))
127122, 123, 126, 119dp34 1179 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((a1 v b1) ^ (a0 v e)) ^ (d v b2)) =< ((a1 v e) v (((a0 v a1) ^ (e v b1)) ^ (((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2)))))
128121, 127bltr 138 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((a1 v b1) ^ (a0 v e)) =< ((a1 v e) v (((a0 v a1) ^ (e v b1)) ^ (((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2)))))
12982, 128lel2or 170 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((a1 v e) v ((a1 v b1) ^ (a0 v e))) =< ((a1 v e) v (((a0 v a1) ^ (e v b1)) ^ (((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2)))))
13081, 129bltr 138 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((a1 v b1) v e) ^ ((a1 v a0) v e)) =< ((a1 v e) v (((a0 v a1) ^ (e v b1)) ^ (((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2)))))
131130lelan 167 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((a0 v a1) ^ (e v b1)) ^ (((a1 v b1) v e) ^ ((a1 v a0) v e))) =< (((a0 v a1) ^ (e v b1)) ^ ((a1 v e) v (((a0 v a1) ^ (e v b1)) ^ (((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2))))))
13260, 131bltr 138 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((a0 v a1) ^ (e v b1)) ^ ((a1 v b1) v e)) ^ ((a1 v a0) v e)) =< (((a0 v a1) ^ (e v b1)) ^ ((a1 v e) v (((a0 v a1) ^ (e v b1)) ^ (((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2))))))
13362, 132bltr 138 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((a0 v a1) ^ (e v b1)) =< (((a0 v a1) ^ (e v b1)) ^ ((a1 v e) v (((a0 v a1) ^ (e v b1)) ^ (((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2))))))
134 mldual 1122 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((a0 v a1) ^ (e v b1)) ^ ((a1 v e) v (((a0 v a1) ^ (e v b1)) ^ (((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2)))))) = ((((a0 v a1) ^ (e v b1)) ^ (a1 v e)) v (((a0 v a1) ^ (e v b1)) ^ (((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2)))))
135 ancom 74 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((a0 v a1) ^ (e v b1)) ^ (((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2)))) = ((((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2))) ^ ((a0 v a1) ^ (e v b1)))
136135lor 70 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((a0 v a1) ^ (e v b1)) ^ (a1 v e)) v (((a0 v a1) ^ (e v b1)) ^ (((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2))))) = ((((a0 v a1) ^ (e v b1)) ^ (a1 v e)) v ((((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2))) ^ ((a0 v a1) ^ (e v b1))))
137 lea 160 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((a0 v a1) ^ (e v b1)) ^ (a1 v e)) =< ((a0 v a1) ^ (e v b1))
138137ml2i 1123 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((a0 v a1) ^ (e v b1)) ^ (a1 v e)) v ((((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2))) ^ ((a0 v a1) ^ (e v b1)))) = (((((a0 v a1) ^ (e v b1)) ^ (a1 v e)) v (((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2)))) ^ ((a0 v a1) ^ (e v b1)))
139 ancom 74 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((a0 v a1) ^ (e v b1)) ^ (a1 v e)) v (((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2)))) ^ ((a0 v a1) ^ (e v b1))) = (((a0 v a1) ^ (e v b1)) ^ ((((a0 v a1) ^ (e v b1)) ^ (a1 v e)) v (((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2)))))
140 ax-a2 31 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((a0 v a1) ^ (e v b1)) ^ (a1 v e)) v (((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2)))) = ((((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2))) v (((a0 v a1) ^ (e v b1)) ^ (a1 v e)))
141140lan 77 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((a0 v a1) ^ (e v b1)) ^ ((((a0 v a1) ^ (e v b1)) ^ (a1 v e)) v (((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2))))) = (((a0 v a1) ^ (e v b1)) ^ ((((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2))) v (((a0 v a1) ^ (e v b1)) ^ (a1 v e))))
142138, 139, 1413tr 65 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((a0 v a1) ^ (e v b1)) ^ (a1 v e)) v ((((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2))) ^ ((a0 v a1) ^ (e v b1)))) = (((a0 v a1) ^ (e v b1)) ^ ((((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2))) v (((a0 v a1) ^ (e v b1)) ^ (a1 v e))))
143134, 136, 1423tr 65 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((a0 v a1) ^ (e v b1)) ^ ((a1 v e) v (((a0 v a1) ^ (e v b1)) ^ (((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2)))))) = (((a0 v a1) ^ (e v b1)) ^ ((((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2))) v (((a0 v a1) ^ (e v b1)) ^ (a1 v e))))
144133, 143lbtr 139 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((a0 v a1) ^ (e v b1)) =< (((a0 v a1) ^ (e v b1)) ^ ((((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2))) v (((a0 v a1) ^ (e v b1)) ^ (a1 v e))))
145 mldual 1122 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((a0 v a1) ^ (e v b1)) ^ ((((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2))) v (((a0 v a1) ^ (e v b1)) ^ (a1 v e)))) = ((((a0 v a1) ^ (e v b1)) ^ (((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2)))) v (((a0 v a1) ^ (e v b1)) ^ (a1 v e)))
14650ran 78 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((a0 v a1) ^ (e v b1)) ^ (a1 v e)) = (((a1 v a0) ^ (b1 v e)) ^ (a1 v e))
147 anass 76 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((a1 v a0) ^ (b1 v e)) ^ (a1 v e)) = ((a1 v a0) ^ ((b1 v e) ^ (a1 v e)))
148 leor 159 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 e =< (b1 v e)
149148mldual2i 1125 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((b1 v e) ^ (a1 v e)) = (((b1 v e) ^ a1) v e)
150 orcom 73 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((b1 v e) ^ a1) v e) = (e v ((b1 v e) ^ a1))
151 ancom 74 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((b1 v e) ^ a1) = (a1 ^ (b1 v e))
152151lor 70 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (e v ((b1 v e) ^ a1)) = (e v (a1 ^ (b1 v e)))
153149, 150, 1523tr 65 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((b1 v e) ^ (a1 v e)) = (e v (a1 ^ (b1 v e)))
154153lan 77 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((a1 v a0) ^ ((b1 v e) ^ (a1 v e))) = ((a1 v a0) ^ (e v (a1 ^ (b1 v e))))
155 leao1 162 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (a1 ^ (b1 v e)) =< (a1 v a0)
156155mldual2i 1125 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((a1 v a0) ^ (e v (a1 ^ (b1 v e)))) = (((a1 v a0) ^ e) v (a1 ^ (b1 v e)))
157 orcom 73 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((a1 v a0) ^ e) v (a1 ^ (b1 v e))) = ((a1 ^ (b1 v e)) v ((a1 v a0) ^ e))
158 ancom 74 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((a1 v a0) ^ e) = (e ^ (a1 v a0))
159158lor 70 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((a1 ^ (b1 v e)) v ((a1 v a0) ^ e)) = ((a1 ^ (b1 v e)) v (e ^ (a1 v a0)))
160157, 159tr 62 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((a1 v a0) ^ e) v (a1 ^ (b1 v e))) = ((a1 ^ (b1 v e)) v (e ^ (a1 v a0)))
161154, 156, 1603tr 65 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((a1 v a0) ^ ((b1 v e) ^ (a1 v e))) = ((a1 ^ (b1 v e)) v (e ^ (a1 v a0)))
162146, 147, 1613tr 65 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((a0 v a1) ^ (e v b1)) ^ (a1 v e)) = ((a1 ^ (b1 v e)) v (e ^ (a1 v a0)))
163162lor 70 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((a0 v a1) ^ (e v b1)) ^ (((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2)))) v (((a0 v a1) ^ (e v b1)) ^ (a1 v e))) = ((((a0 v a1) ^ (e v b1)) ^ (((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2)))) v ((a1 ^ (b1 v e)) v (e ^ (a1 v a0))))
164145, 163tr 62 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((a0 v a1) ^ (e v b1)) ^ ((((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2))) v (((a0 v a1) ^ (e v b1)) ^ (a1 v e)))) = ((((a0 v a1) ^ (e v b1)) ^ (((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2)))) v ((a1 ^ (b1 v e)) v (e ^ (a1 v a0))))
165 lear 161 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((a0 v a1) ^ (e v b1)) ^ (((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2)))) =< (((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2)))
166165leror 152 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((a0 v a1) ^ (e v b1)) ^ (((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2)))) v ((a1 ^ (b1 v e)) v (e ^ (a1 v a0)))) =< ((((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2))) v ((a1 ^ (b1 v e)) v (e ^ (a1 v a0))))
167164, 166bltr 138 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((a0 v a1) ^ (e v b1)) ^ ((((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2))) v (((a0 v a1) ^ (e v b1)) ^ (a1 v e)))) =< ((((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2))) v ((a1 ^ (b1 v e)) v (e ^ (a1 v a0))))
168144, 167letr 137 . . . . . . . . . . . . . . . . . . . . . . . 24 ((a0 v a1) ^ (e v b1)) =< ((((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2))) v ((a1 ^ (b1 v e)) v (e ^ (a1 v a0))))
169 orcom 73 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((a1 ^ (b1 v e)) v (e ^ (a1 v a0))) = ((e ^ (a1 v a0)) v (a1 ^ (b1 v e)))
170169lor 70 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2))) v ((a1 ^ (b1 v e)) v (e ^ (a1 v a0)))) = ((((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2))) v ((e ^ (a1 v a0)) v (a1 ^ (b1 v e))))
171 or4 84 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2))) v ((e ^ (a1 v a0)) v (a1 ^ (b1 v e)))) = ((((a0 v d) ^ (e v b2)) v (e ^ (a1 v a0))) v (((a1 v d) ^ (b1 v b2)) v (a1 ^ (b1 v e))))
172 ancom 74 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((a0 v d) ^ (e v b2)) = ((e v b2) ^ (a0 v d))
173122, 172tr 62 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((a0 v d) ^ (e v b2)) = ((e v b2) ^ (a0 v d))
174173ror 71 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((a0 v d) ^ (e v b2)) v (e ^ (a1 v a0))) = (((e v b2) ^ (a0 v d)) v (e ^ (a1 v a0)))
175123ror 71 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((a1 v d) ^ (b1 v b2)) v (a1 ^ (b1 v e))) = (((a1 v d) ^ (b1 v b2)) v (a1 ^ (b1 v e)))
176174, 1752or 72 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((a0 v d) ^ (e v b2)) v (e ^ (a1 v a0))) v (((a1 v d) ^ (b1 v b2)) v (a1 ^ (b1 v e)))) = ((((e v b2) ^ (a0 v d)) v (e ^ (a1 v a0))) v (((a1 v d) ^ (b1 v b2)) v (a1 ^ (b1 v e))))
177171, 176tr 62 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2))) v ((e ^ (a1 v a0)) v (a1 ^ (b1 v e)))) = ((((e v b2) ^ (a0 v d)) v (e ^ (a1 v a0))) v (((a1 v d) ^ (b1 v b2)) v (a1 ^ (b1 v e))))
178 leao1 162 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (e ^ (a1 v a0)) =< (e v b2)
179178mli 1124 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((e v b2) ^ (a0 v d)) v (e ^ (a1 v a0))) = ((e v b2) ^ ((a0 v d) v (e ^ (a1 v a0))))
180 leao1 162 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (a1 ^ (b1 v e)) =< (a1 v d)
181180mli 1124 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((a1 v d) ^ (b1 v b2)) v (a1 ^ (b1 v e))) = ((a1 v d) ^ ((b1 v b2) v (a1 ^ (b1 v e))))
182179, 1812or 72 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((e v b2) ^ (a0 v d)) v (e ^ (a1 v a0))) v (((a1 v d) ^ (b1 v b2)) v (a1 ^ (b1 v e)))) = (((e v b2) ^ ((a0 v d) v (e ^ (a1 v a0)))) v ((a1 v d) ^ ((b1 v b2) v (a1 ^ (b1 v e)))))
183170, 177, 1823tr 65 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2))) v ((a1 ^ (b1 v e)) v (e ^ (a1 v a0)))) = (((e v b2) ^ ((a0 v d) v (e ^ (a1 v a0)))) v ((a1 v d) ^ ((b1 v b2) v (a1 ^ (b1 v e)))))
184 or32 82 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((a0 v d) v (e ^ (a1 v a0))) = ((a0 v (e ^ (a1 v a0))) v d)
185 ml3 1128 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (a0 v (e ^ (a1 v a0))) = (a0 v (a1 ^ (e v a0)))
186 orcom 73 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (e v a0) = (a0 v e)
187186lan 77 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (a1 ^ (e v a0)) = (a1 ^ (a0 v e))
188187lor 70 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (a0 v (a1 ^ (e v a0))) = (a0 v (a1 ^ (a0 v e)))
189185, 188tr 62 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (a0 v (e ^ (a1 v a0))) = (a0 v (a1 ^ (a0 v e)))
190189ror 71 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((a0 v (e ^ (a1 v a0))) v d) = ((a0 v (a1 ^ (a0 v e))) v d)
191 or32 82 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((a0 v (a1 ^ (a0 v e))) v d) = ((a0 v d) v (a1 ^ (a0 v e)))
192184, 190, 1913tr 65 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((a0 v d) v (e ^ (a1 v a0))) = ((a0 v d) v (a1 ^ (a0 v e)))
193192lan 77 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((e v b2) ^ ((a0 v d) v (e ^ (a1 v a0)))) = ((e v b2) ^ ((a0 v d) v (a1 ^ (a0 v e))))
194 or32 82 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((b1 v b2) v (a1 ^ (b1 v e))) = ((b1 v (a1 ^ (b1 v e))) v b2)
195 orcom 73 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (b1 v e) = (e v b1)
196195lan 77 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (a1 ^ (b1 v e)) = (a1 ^ (e v b1))
197196lor 70 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (b1 v (a1 ^ (b1 v e))) = (b1 v (a1 ^ (e v b1)))
198 ml3 1128 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (b1 v (a1 ^ (e v b1))) = (b1 v (e ^ (a1 v b1)))
199197, 198tr 62 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (b1 v (a1 ^ (b1 v e))) = (b1 v (e ^ (a1 v b1)))
200199ror 71 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((b1 v (a1 ^ (b1 v e))) v b2) = ((b1 v (e ^ (a1 v b1))) v b2)
201 or32 82 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((b1 v (e ^ (a1 v b1))) v b2) = ((b1 v b2) v (e ^ (a1 v b1)))
202194, 200, 2013tr 65 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((b1 v b2) v (a1 ^ (b1 v e))) = ((b1 v b2) v (e ^ (a1 v b1)))
203202lan 77 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((a1 v d) ^ ((b1 v b2) v (a1 ^ (b1 v e)))) = ((a1 v d) ^ ((b1 v b2) v (e ^ (a1 v b1))))
204193, 2032or 72 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((e v b2) ^ ((a0 v d) v (e ^ (a1 v a0)))) v ((a1 v d) ^ ((b1 v b2) v (a1 ^ (b1 v e))))) = (((e v b2) ^ ((a0 v d) v (a1 ^ (a0 v e)))) v ((a1 v d) ^ ((b1 v b2) v (e ^ (a1 v b1)))))
205183, 204tr 62 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2))) v ((a1 ^ (b1 v e)) v (e ^ (a1 v a0)))) = (((e v b2) ^ ((a0 v d) v (a1 ^ (a0 v e)))) v ((a1 v d) ^ ((b1 v b2) v (e ^ (a1 v b1)))))
206168, 205lbtr 139 . . . . . . . . . . . . . . . . . . . . . . 23 ((a0 v a1) ^ (e v b1)) =< (((e v b2) ^ ((a0 v d) v (a1 ^ (a0 v e)))) v ((a1 v d) ^ ((b1 v b2) v (e ^ (a1 v b1)))))
207 lea 160 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (a1 ^ (a0 v e)) =< a1
20874leran 153 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (a1 ^ (a0 v e)) =< ((a1 v b1) ^ (a0 v e))
209208, 116letr 137 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (a1 ^ (a0 v e)) =< (d v b2)
210207, 209ler2an 173 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (a1 ^ (a0 v e)) =< (a1 ^ (d v b2))
211210lelor 166 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((a0 v d) v (a1 ^ (a0 v e))) =< ((a0 v d) v (a1 ^ (d v b2)))
212211lelan 167 . . . . . . . . . . . . . . . . . . . . . . . 24 ((e v b2) ^ ((a0 v d) v (a1 ^ (a0 v e)))) =< ((e v b2) ^ ((a0 v d) v (a1 ^ (d v b2))))
213 lea 160 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (e ^ (a1 v b1)) =< e
214 lear 161 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (e ^ (a1 v b1)) =< (a1 v b1)
215 leao3 164 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (e ^ (a1 v b1)) =< (a0 v e)
216214, 215ler2an 173 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (e ^ (a1 v b1)) =< ((a1 v b1) ^ (a0 v e))
217216, 116letr 137 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (e ^ (a1 v b1)) =< (d v b2)
218213, 217ler2an 173 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (e ^ (a1 v b1)) =< (e ^ (d v b2))
219218lelor 166 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((b1 v b2) v (e ^ (a1 v b1))) =< ((b1 v b2) v (e ^ (d v b2)))
220219lelan 167 . . . . . . . . . . . . . . . . . . . . . . . 24 ((a1 v d) ^ ((b1 v b2) v (e ^ (a1 v b1)))) =< ((a1 v d) ^ ((b1 v b2) v (e ^ (d v b2))))
221212, 220le2or 168 . . . . . . . . . . . . . . . . . . . . . . 23 (((e v b2) ^ ((a0 v d) v (a1 ^ (a0 v e)))) v ((a1 v d) ^ ((b1 v b2) v (e ^ (a1 v b1))))) =< (((e v b2) ^ ((a0 v d) v (a1 ^ (d v b2)))) v ((a1 v d) ^ ((b1 v b2) v (e ^ (d v b2)))))
222206, 221letr 137 . . . . . . . . . . . . . . . . . . . . . 22 ((a0 v a1) ^ (e v b1)) =< (((e v b2) ^ ((a0 v d) v (a1 ^ (d v b2)))) v ((a1 v d) ^ ((b1 v b2) v (e ^ (d v b2)))))
223 ax-a2 31 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (d v b2) = (b2 v d)
224223lan 77 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (a1 ^ (d v b2)) = (a1 ^ (b2 v d))
225224lor 70 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (d v (a1 ^ (d v b2))) = (d v (a1 ^ (b2 v d)))
226 ml3 1128 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (d v (a1 ^ (b2 v d))) = (d v (b2 ^ (a1 v d)))
227225, 226tr 62 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (d v (a1 ^ (d v b2))) = (d v (b2 ^ (a1 v d)))
228227lor 70 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (a0 v (d v (a1 ^ (d v b2)))) = (a0 v (d v (b2 ^ (a1 v d))))
229 orass 75 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((a0 v d) v (a1 ^ (d v b2))) = (a0 v (d v (a1 ^ (d v b2))))
230 orass 75 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((a0 v d) v (b2 ^ (a1 v d))) = (a0 v (d v (b2 ^ (a1 v d))))
231228, 229, 2303tr1 63 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((a0 v d) v (a1 ^ (d v b2))) = ((a0 v d) v (b2 ^ (a1 v d)))
232231lan 77 . . . . . . . . . . . . . . . . . . . . . . . 24 ((e v b2) ^ ((a0 v d) v (a1 ^ (d v b2)))) = ((e v b2) ^ ((a0 v d) v (b2 ^ (a1 v d))))
233 ml3 1128 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (b2 v (e ^ (d v b2))) = (b2 v (d ^ (e v b2)))
234233lor 70 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (b1 v (b2 v (e ^ (d v b2)))) = (b1 v (b2 v (d ^ (e v b2))))
235 orass 75 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((b1 v b2) v (e ^ (d v b2))) = (b1 v (b2 v (e ^ (d v b2))))
236 orass 75 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((b1 v b2) v (d ^ (e v b2))) = (b1 v (b2 v (d ^ (e v b2))))
237234, 235, 2363tr1 63 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((b1 v b2) v (e ^ (d v b2))) = ((b1 v b2) v (d ^ (e v b2)))
238237lan 77 . . . . . . . . . . . . . . . . . . . . . . . 24 ((a1 v d) ^ ((b1 v b2) v (e ^ (d v b2)))) = ((a1 v d) ^ ((b1 v b2) v (d ^ (e v b2))))
239232, 2382or 72 . . . . . . . . . . . . . . . . . . . . . . 23 (((e v b2) ^ ((a0 v d) v (a1 ^ (d v b2)))) v ((a1 v d) ^ ((b1 v b2) v (e ^ (d v b2))))) = (((e v b2) ^ ((a0 v d) v (b2 ^ (a1 v d)))) v ((a1 v d) ^ ((b1 v b2) v (d ^ (e v b2)))))
240 leao3 164 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (b2 ^ (a1 v d)) =< (e v b2)
241240mldual2i 1125 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((e v b2) ^ ((a0 v d) v (b2 ^ (a1 v d)))) = (((e v b2) ^ (a0 v d)) v (b2 ^ (a1 v d)))
242173ror 71 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((a0 v d) ^ (e v b2)) v (b2 ^ (a1 v d))) = (((e v b2) ^ (a0 v d)) v (b2 ^ (a1 v d)))
243242cm 61 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((e v b2) ^ (a0 v d)) v (b2 ^ (a1 v d))) = (((a0 v d) ^ (e v b2)) v (b2 ^ (a1 v d)))
244241, 243tr 62 . . . . . . . . . . . . . . . . . . . . . . . 24 ((e v b2) ^ ((a0 v d) v (b2 ^ (a1 v d)))) = (((a0 v d) ^ (e v b2)) v (b2 ^ (a1 v d)))
245 leao3 164 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (d ^ (e v b2)) =< (a1 v d)
246245mldual2i 1125 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((a1 v d) ^ ((b1 v b2) v (d ^ (e v b2)))) = (((a1 v d) ^ (b1 v b2)) v (d ^ (e v b2)))
247123ror 71 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((a1 v d) ^ (b1 v b2)) v (d ^ (e v b2))) = (((a1 v d) ^ (b1 v b2)) v (d ^ (e v b2)))
248247cm 61 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((a1 v d) ^ (b1 v b2)) v (d ^ (e v b2))) = (((a1 v d) ^ (b1 v b2)) v (d ^ (e v b2)))
249246, 248tr 62 . . . . . . . . . . . . . . . . . . . . . . . 24 ((a1 v d) ^ ((b1 v b2) v (d ^ (e v b2)))) = (((a1 v d) ^ (b1 v b2)) v (d ^ (e v b2)))
250244, 2492or 72 . . . . . . . . . . . . . . . . . . . . . . 23 (((e v b2) ^ ((a0 v d) v (b2 ^ (a1 v d)))) v ((a1 v d) ^ ((b1 v b2) v (d ^ (e v b2))))) = ((((a0 v d) ^ (e v b2)) v (b2 ^ (a1 v d))) v (((a1 v d) ^ (b1 v b2)) v (d ^ (e v b2))))
251 or4 84 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((a0 v d) ^ (e v b2)) v (b2 ^ (a1 v d))) v (((a1 v d) ^ (b1 v b2)) v (d ^ (e v b2)))) = ((((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2))) v ((b2 ^ (a1 v d)) v (d ^ (e v b2))))
252 orcom 73 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2))) v ((b2 ^ (a1 v d)) v (d ^ (e v b2)))) = (((b2 ^ (a1 v d)) v (d ^ (e v b2))) v (((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2))))
253 ancom 74 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (b2 ^ (a1 v d)) = ((a1 v d) ^ b2)
254 leor 159 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 b2 =< (b1 v b2)
255254lelan 167 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((a1 v d) ^ b2) =< ((a1 v d) ^ (b1 v b2))
256253, 255bltr 138 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (b2 ^ (a1 v d)) =< ((a1 v d) ^ (b1 v b2))
257 leor 159 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 d =< (a0 v d)
258257leran 153 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (d ^ (e v b2)) =< ((a0 v d) ^ (e v b2))
259256, 258le2or 168 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((b2 ^ (a1 v d)) v (d ^ (e v b2))) =< (((a1 v d) ^ (b1 v b2)) v ((a0 v d) ^ (e v b2)))
260123, 1222or 72 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((a1 v d) ^ (b1 v b2)) v ((a0 v d) ^ (e v b2))) = (((a1 v d) ^ (b1 v b2)) v ((a0 v d) ^ (e v b2)))
261260cm 61 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((a1 v d) ^ (b1 v b2)) v ((a0 v d) ^ (e v b2))) = (((a1 v d) ^ (b1 v b2)) v ((a0 v d) ^ (e v b2)))
262 orcom 73 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((a1 v d) ^ (b1 v b2)) v ((a0 v d) ^ (e v b2))) = (((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2)))
263261, 262tr 62 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((a1 v d) ^ (b1 v b2)) v ((a0 v d) ^ (e v b2))) = (((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2)))
264259, 263lbtr 139 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((b2 ^ (a1 v d)) v (d ^ (e v b2))) =< (((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2)))
265264df-le2 131 . . . . . . . . . . . . . . . . . . . . . . . 24 (((b2 ^ (a1 v d)) v (d ^ (e v b2))) v (((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2)))) = (((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2)))
266251, 252, 2653tr 65 . . . . . . . . . . . . . . . . . . . . . . 23 ((((a0 v d) ^ (e v b2)) v (b2 ^ (a1 v d))) v (((a1 v d) ^ (b1 v b2)) v (d ^ (e v b2)))) = (((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2)))
267239, 250, 2663tr 65 . . . . . . . . . . . . . . . . . . . . . 22 (((e v b2) ^ ((a0 v d) v (a1 ^ (d v b2)))) v ((a1 v d) ^ ((b1 v b2) v (e ^ (d v b2))))) = (((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2)))
268222, 267lbtr 139 . . . . . . . . . . . . . . . . . . . . 21 ((a0 v a1) ^ (e v b1)) =< (((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2)))
26985ror 71 . . . . . . . . . . . . . . . . . . . . . 22 (e v b1) = ((b0 ^ (a0 v p0)) v b1)
270269lan 77 . . . . . . . . . . . . . . . . . . . . 21 ((a0 v a1) ^ (e v b1)) = ((a0 v a1) ^ ((b0 ^ (a0 v p0)) v b1))
271109lor 70 . . . . . . . . . . . . . . . . . . . . . . 23 (a0 v d) = (a0 v (a2 v (a0 ^ (a1 v b1))))
27285ror 71 . . . . . . . . . . . . . . . . . . . . . . 23 (e v b2) = ((b0 ^ (a0 v p0)) v b2)
273271, 2722an 79 . . . . . . . . . . . . . . . . . . . . . 22 ((a0 v d) ^ (e v b2)) = ((a0 v (a2 v (a0 ^ (a1 v b1)))) ^ ((b0 ^ (a0 v p0)) v b2))
274109lor 70 . . . . . . . . . . . . . . . . . . . . . . 23 (a1 v d) = (a1 v (a2 v (a0 ^ (a1 v b1))))
275274ran 78 . . . . . . . . . . . . . . . . . . . . . 22 ((a1 v d) ^ (b1 v b2)) = ((a1 v (a2 v (a0 ^ (a1 v b1)))) ^ (b1 v b2))
276273, 2752or 72 . . . . . . . . . . . . . . . . . . . . 21 (((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2))) = (((a0 v (a2 v (a0 ^ (a1 v b1)))) ^ ((b0 ^ (a0 v p0)) v b2)) v ((a1 v (a2 v (a0 ^ (a1 v b1)))) ^ (b1 v b2)))
277268, 270, 276le3tr2 141 . . . . . . . . . . . . . . . . . . . 20 ((a0 v a1) ^ ((b0 ^ (a0 v p0)) v b1)) =< (((a0 v (a2 v (a0 ^ (a1 v b1)))) ^ ((b0 ^ (a0 v p0)) v b2)) v ((a1 v (a2 v (a0 ^ (a1 v b1)))) ^ (b1 v b2)))
278 or12 80 . . . . . . . . . . . . . . . . . . . . . . 23 (a0 v (a2 v (a0 ^ (a1 v b1)))) = (a2 v (a0 v (a0 ^ (a1 v b1))))
279 orabs 120 . . . . . . . . . . . . . . . . . . . . . . . 24 (a0 v (a0 ^ (a1 v b1))) = a0
280279lor 70 . . . . . . . . . . . . . . . . . . . . . . 23 (a2 v (a0 v (a0 ^ (a1 v b1)))) = (a2 v a0)
281 orcom 73 . . . . . . . . . . . . . . . . . . . . . . 23 (a2 v a0) = (a0 v a2)
282278, 280, 2813tr 65 . . . . . . . . . . . . . . . . . . . . . 22 (a0 v (a2 v (a0 ^ (a1 v b1)))) = (a0 v a2)
283282ran 78 . . . . . . . . . . . . . . . . . . . . 21 ((a0 v (a2 v (a0 ^ (a1 v b1)))) ^ ((b0 ^ (a0 v p0)) v b2)) = ((a0 v a2) ^ ((b0 ^ (a0 v p0)) v b2))
284 orass 75 . . . . . . . . . . . . . . . . . . . . . . 23 ((a1 v a2) v (a0 ^ (a1 v b1))) = (a1 v (a2 v (a0 ^ (a1 v b1))))
285284ran 78 . . . . . . . . . . . . . . . . . . . . . 22 (((a1 v a2) v (a0 ^ (a1 v b1))) ^ (b1 v b2)) = ((a1 v (a2 v (a0 ^ (a1 v b1)))) ^ (b1 v b2))
286285cm 61 . . . . . . . . . . . . . . . . . . . . 21 ((a1 v (a2 v (a0 ^ (a1 v b1)))) ^ (b1 v b2)) = (((a1 v a2) v (a0 ^ (a1 v b1))) ^ (b1 v b2))
287283, 2862or 72 . . . . . . . . . . . . . . . . . . . 20 (((a0 v (a2 v (a0 ^ (a1 v b1)))) ^ ((b0 ^ (a0 v p0)) v b2)) v ((a1 v (a2 v (a0 ^ (a1 v b1)))) ^ (b1 v b2))) = (((a0 v a2) ^ ((b0 ^ (a0 v p0)) v b2)) v (((a1 v a2) v (a0 ^ (a1 v b1))) ^ (b1 v b2)))
288277, 287lbtr 139 . . . . . . . . . . . . . . . . . . 19 ((a0 v a1) ^ ((b0 ^ (a0 v p0)) v b1)) =< (((a0 v a2) ^ ((b0 ^ (a0 v p0)) v b2)) v (((a1 v a2) v (a0 ^ (a1 v b1))) ^ (b1 v b2)))
289 ax-a2 31 . . . . . . . . . . . . . . . . . . . . . . . . 25 (a1 v a2) = (a2 v a1)
290 ax-a2 31 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (a1 v b1) = (b1 v a1)
291290lan 77 . . . . . . . . . . . . . . . . . . . . . . . . 25 (a0 ^ (a1 v b1)) = (a0 ^ (b1 v a1))
292289, 2912or 72 . . . . . . . . . . . . . . . . . . . . . . . 24 ((a1 v a2) v (a0 ^ (a1 v b1))) = ((a2 v a1) v (a0 ^ (b1 v a1)))
293 orass 75 . . . . . . . . . . . . . . . . . . . . . . . 24 ((a2 v a1) v (a0 ^ (b1 v a1))) = (a2 v (a1 v (a0 ^ (b1 v a1))))
294292, 293tr 62 . . . . . . . . . . . . . . . . . . . . . . 23 ((a1 v a2) v (a0 ^ (a1 v b1))) = (a2 v (a1 v (a0 ^ (b1 v a1))))
295 ml3le 1127 . . . . . . . . . . . . . . . . . . . . . . . 24 (a1 v (a0 ^ (b1 v a1))) =< (a1 v (b1 ^ (a0 v a1)))
296295lelor 166 . . . . . . . . . . . . . . . . . . . . . . 23 (a2 v (a1 v (a0 ^ (b1 v a1)))) =< (a2 v (a1 v (b1 ^ (a0 v a1))))
297294, 296bltr 138 . . . . . . . . . . . . . . . . . . . . . 22 ((a1 v a2) v (a0 ^ (a1 v b1))) =< (a2 v (a1 v (b1 ^ (a0 v a1))))
298 orass 75 . . . . . . . . . . . . . . . . . . . . . . . 24 ((a2 v a1) v (b1 ^ (a0 v a1))) = (a2 v (a1 v (b1 ^ (a0 v a1))))
299298cm 61 . . . . . . . . . . . . . . . . . . . . . . 23 (a2 v (a1 v (b1 ^ (a0 v a1)))) = ((a2 v a1) v (b1 ^ (a0 v a1)))
300 ax-a2 31 . . . . . . . . . . . . . . . . . . . . . . . 24 (a2 v a1) = (a1 v a2)
301300ror 71 . . . . . . . . . . . . . . . . . . . . . . 23 ((a2 v a1) v (b1 ^ (a0 v a1))) = ((a1 v a2) v (b1 ^ (a0 v a1)))
302299, 301tr 62 . . . . . . . . . . . . . . . . . . . . . 22 (a2 v (a1 v (b1 ^ (a0 v a1)))) = ((a1 v a2) v (b1 ^ (a0 v a1)))
303297, 302lbtr 139 . . . . . . . . . . . . . . . . . . . . 21 ((a1 v a2) v (a0 ^ (a1 v b1))) =< ((a1 v a2) v (b1 ^ (a0 v a1)))
304303leran 153 . . . . . . . . . . . . . . . . . . . 20 (((a1 v a2) v (a0 ^ (a1 v b1))) ^ (b1 v b2)) =< (((a1 v a2) v (b1 ^ (a0 v a1))) ^ (b1 v b2))
305304lelor 166 . . . . . . . . . . . . . . . . . . 19 (((a0 v a2) ^ ((b0 ^ (a0 v p0)) v b2)) v (((a1 v a2) v (a0 ^ (a1 v b1))) ^ (b1 v b2))) =< (((a0 v a2) ^ ((b0 ^ (a0 v p0)) v b2)) v (((a1 v a2) v (b1 ^ (a0 v a1))) ^ (b1 v b2)))
306288, 305letr 137 . . . . . . . . . . . . . . . . . 18 ((a0 v a1) ^ ((b0 ^ (a0 v p0)) v b1)) =< (((a0 v a2) ^ ((b0 ^ (a0 v p0)) v b2)) v (((a1 v a2) v (b1 ^ (a0 v a1))) ^ (b1 v b2)))
30724leror 152 . . . . . . . . . . . . . . . . . . . . 21 ((b0 ^ (a0 v p0)) v b2) =< (b0 v b2)
308307lelan 167 . . . . . . . . . . . . . . . . . . . 20 ((a0 v a2) ^ ((b0 ^ (a0 v p0)) v b2)) =< ((a0 v a2) ^ (b0 v b2))
309 leao1 162 . . . . . . . . . . . . . . . . . . . . . . 23 (b1 ^ (a0 v a1)) =< (b1 v b2)
310309mldual2i 1125 . . . . . . . . . . . . . . . . . . . . . 22 ((b1 v b2) ^ ((a1 v a2) v (b1 ^ (a0 v a1)))) = (((b1 v b2) ^ (a1 v a2)) v (b1 ^ (a0 v a1)))
311 ancom 74 . . . . . . . . . . . . . . . . . . . . . 22 ((b1 v b2) ^ ((a1 v a2) v (b1 ^ (a0 v a1)))) = (((a1 v a2) v (b1 ^ (a0 v a1))) ^ (b1 v b2))
312 ancom 74 . . . . . . . . . . . . . . . . . . . . . . 23 ((b1 v b2) ^ (a1 v a2)) = ((a1 v a2) ^ (b1 v b2))
313312ror 71 . . . . . . . . . . . . . . . . . . . . . 22 (((b1 v b2) ^ (a1 v a2)) v (b1 ^ (a0 v a1))) = (((a1 v a2) ^ (b1 v b2)) v (b1 ^ (a0 v a1)))
314310, 311, 3133tr2 64 . . . . . . . . . . . . . . . . . . . . 21 (((a1 v a2) v (b1 ^ (a0 v a1))) ^ (b1 v b2)) = (((a1 v a2) ^ (b1 v b2)) v (b1 ^ (a0 v a1)))
315314bile 142 . . . . . . . . . . . . . . . . . . . 20 (((a1 v a2) v (b1 ^ (a0 v a1))) ^ (b1 v b2)) =< (((a1 v a2) ^ (b1 v b2)) v (b1 ^ (a0 v a1)))
316308, 315le2or 168 . . . . . . . . . . . . . . . . . . 19 (((a0 v a2) ^ ((b0 ^ (a0 v p0)) v b2)) v (((a1 v a2) v (b1 ^ (a0 v a1))) ^ (b1 v b2))) =< (((a0 v a2) ^ (b0 v b2)) v (((a1 v a2) ^ (b1 v b2)) v (b1 ^ (a0 v a1))))
317 or12 80 . . . . . . . . . . . . . . . . . . 19 (((a0 v a2) ^ (b0 v b2)) v (((a1 v a2) ^ (b1 v b2)) v (b1 ^ (a0 v a1)))) = (((a1 v a2) ^ (b1 v b2)) v (((a0 v a2) ^ (b0 v b2)) v (b1 ^ (a0 v a1))))
318316, 317lbtr 139 . . . . . . . . . . . . . . . . . 18 (((a0 v a2) ^ ((b0 ^ (a0 v p0)) v b2)) v (((a1 v a2) v (b1 ^ (a0 v a1))) ^ (b1 v b2))) =< (((a1 v a2) ^ (b1 v b2)) v (((a0 v a2) ^ (b0 v b2)) v (b1 ^ (a0 v a1))))
319306, 318letr 137 . . . . . . . . . . . . . . . . 17 ((a0 v a1) ^ ((b0 ^ (a0 v p0)) v b1)) =< (((a1 v a2) ^ (b1 v b2)) v (((a0 v a2) ^ (b0 v b2)) v (b1 ^ (a0 v a1))))
320 xxdp.c0 . . . . . . . . . . . . . . . . . . . 20 c0 = ((a1 v a2) ^ (b1 v b2))
321 xxdp.c1 . . . . . . . . . . . . . . . . . . . . 21 c1 = ((a0 v a2) ^ (b0 v b2))
322321ror 71 . . . . . . . . . . . . . . . . . . . 20 (c1 v (b1 ^ (a0 v a1))) = (((a0 v a2) ^ (b0 v b2)) v (b1 ^ (a0 v a1)))
323320, 3222or 72 . . . . . . . . . . . . . . . . . . 19 (c0 v (c1 v (b1 ^ (a0 v a1)))) = (((a1 v a2) ^ (b1 v b2)) v (((a0 v a2) ^ (b0 v b2)) v (b1 ^ (a0 v a1))))
324323cm 61 . . . . . . . . . . . . . . . . . 18 (((a1 v a2) ^ (b1 v b2)) v (((a0 v a2) ^ (b0 v b2)) v (b1 ^ (a0 v a1)))) = (c0 v (c1 v (b1 ^ (a0 v a1))))
325 orass 75 . . . . . . . . . . . . . . . . . . 19 ((c0 v c1) v (b1 ^ (a0 v a1))) = (c0 v (c1 v (b1 ^ (a0 v a1))))
326325cm 61 . . . . . . . . . . . . . . . . . 18 (c0 v (c1 v (b1 ^ (a0 v a1)))) = ((c0 v c1) v (b1 ^ (a0 v a1)))
327324, 326tr 62 . . . . . . . . . . . . . . . . 17 (((a1 v a2) ^ (b1 v b2)) v (((a0 v a2) ^ (b0 v b2)) v (b1 ^ (a0 v a1)))) = ((c0 v c1) v (b1 ^ (a0 v a1)))
328319, 327lbtr 139 . . . . . . . . . . . . . . . 16 ((a0 v a1) ^ ((b0 ^ (a0 v p0)) v b1)) =< ((c0 v c1) v (b1 ^ (a0 v a1)))
32947, 328ler2an 173 . . . . . . . . . . . . . . 15 ((a0 v a1) ^ ((b0 ^ (a0 v p0)) v b1)) =< ((a0 v a1) ^ ((c0 v c1) v (b1 ^ (a0 v a1))))
330 lear 161 . . . . . . . . . . . . . . . 16 (b1 ^ (a0 v a1)) =< (a0 v a1)
331330mldual2i 1125 . . . . . . . . . . . . . . 15 ((a0 v a1) ^ ((c0 v c1) v (b1 ^ (a0 v a1)))) = (((a0 v a1) ^ (c0 v c1)) v (b1 ^ (a0 v a1)))
332329, 331lbtr 139 . . . . . . . . . . . . . 14 ((a0 v a1) ^ ((b0 ^ (a0 v p0)) v b1)) =< (((a0 v a1) ^ (c0 v c1)) v (b1 ^ (a0 v a1)))
333 lea 160 . . . . . . . . . . . . . . 15 (b1 ^ (a0 v a1)) =< b1
334333lelor 166 . . . . . . . . . . . . . 14 (((a0 v a1) ^ (c0 v c1)) v (b1 ^ (a0 v a1))) =< (((a0 v a1) ^ (c0 v c1)) v b1)
335332, 334letr 137 . . . . . . . . . . . . 13 ((a0 v a1) ^ ((b0 ^ (a0 v p0)) v b1)) =< (((a0 v a1) ^ (c0 v c1)) v b1)
336 orcom 73 . . . . . . . . . . . . 13 (((a0 v a1) ^ (c0 v c1)) v b1) = (b1 v ((a0 v a1) ^ (c0 v c1)))
337335, 336lbtr 139 . . . . . . . . . . . 12 ((a0 v a1) ^ ((b0 ^ (a0 v p0)) v b1)) =< (b1 v ((a0 v a1) ^ (c0 v c1)))
338 leid 148 . . . . . . . . . . . 12 (b1 v ((a0 v a1) ^ (c0 v c1))) =< (b1 v ((a0 v a1) ^ (c0 v c1)))
339337, 338lel2or 170 . . . . . . . . . . 11 (((a0 v a1) ^ ((b0 ^ (a0 v p0)) v b1)) v (b1 v ((a0 v a1) ^ (c0 v c1)))) =< (b1 v ((a0 v a1) ^ (c0 v c1)))
34046, 339letr 137 . . . . . . . . . 10 (b0 ^ (a0 v p0)) =< (b1 v ((a0 v a1) ^ (c0 v c1)))
34126, 340lel2or 170 . . . . . . . . 9 (b1 v (b0 ^ (a0 v p0))) =< (b1 v ((a0 v a1) ^ (c0 v c1)))
34225, 341letr 137 . . . . . . . 8 (b0 ^ (a0 v p0)) =< (b1 v ((a0 v a1) ^ (c0 v c1)))
34324, 342ler2an 173 . . . . . . 7 (b0 ^ (a0 v p0)) =< (b0 ^ (b1 v ((a0 v a1) ^ (c0 v c1))))
344 or32 82 . . . . . . . . . . 11 (((a0 ^ b0) v b1) v (c2 ^ (c0 v c1))) = (((a0 ^ b0) v (c2 ^ (c0 v c1))) v b1)
345 orcom 73 . . . . . . . . . . 11 (((a0 ^ b0) v (c2 ^ (c0 v c1))) v b1) = (b1 v ((a0 ^ b0) v (c2 ^ (c0 v c1))))
346 leo 158 . . . . . . . . . . . . . . . 16 a0 =< (a0 v a1)
347 leo 158 . . . . . . . . . . . . . . . 16 b0 =< (b0 v b1)
348346, 347le2an 169 . . . . . . . . . . . . . . 15 (a0 ^ b0) =< ((a0 v a1) ^ (b0 v b1))
349 xxdp.c2 . . . . . . . . . . . . . . . 16 c2 = ((a0 v a1) ^ (b0 v b1))
350349cm 61 . . . . . . . . . . . . . . 15 ((a0 v a1) ^ (b0 v b1)) = c2
351348, 350lbtr 139 . . . . . . . . . . . . . 14 (a0 ^ b0) =< c2
352 leo 158 . . . . . . . . . . . . . . . . 17 a0 =< (a0 v a2)
353 leo 158 . . . . . . . . . . . . . . . . 17 b0 =< (b0 v b2)
354352, 353le2an 169 . . . . . . . . . . . . . . . 16 (a0 ^ b0) =< ((a0 v a2) ^ (b0 v b2))
355321cm 61 . . . . . . . . . . . . . . . 16 ((a0 v a2) ^ (b0 v b2)) = c1
356354, 355lbtr 139 . . . . . . . . . . . . . . 15 (a0 ^ b0) =< c1
357356lerr 150 . . . . . . . . . . . . . 14 (a0 ^ b0) =< (c0 v c1)
358351, 357ler2an 173 . . . . . . . . . . . . 13 (a0 ^ b0) =< (c2 ^ (c0 v c1))
359358df-le2 131 . . . . . . . . . . . 12 ((a0 ^ b0) v (c2 ^ (c0 v c1))) = (c2 ^ (c0 v c1))
360359lor 70 . . . . . . . . . . 11 (b1 v ((a0 ^ b0) v (c2 ^ (c0 v c1)))) = (b1 v (c2 ^ (c0 v c1)))
361344, 345, 3603tr 65 . . . . . . . . . 10 (((a0 ^ b0) v b1) v (c2 ^ (c0 v c1))) = (b1 v (c2 ^ (c0 v c1)))
362361lan 77 . . . . . . . . 9 (b0 ^ (((a0 ^ b0) v b1) v (c2 ^ (c0 v c1)))) = (b0 ^ (b1 v (c2 ^ (c0 v c1))))
363349ran 78 . . . . . . . . . . . . . 14 (c2 ^ (c0 v c1)) = (((a0 v a1) ^ (b0 v b1)) ^ (c0 v c1))
364 an32 83 . . . . . . . . . . . . . 14 (((a0 v a1) ^ (b0 v b1)) ^ (c0 v c1)) = (((a0 v a1) ^ (c0 v c1)) ^ (b0 v b1))
365363, 364tr 62 . . . . . . . . . . . . 13 (c2 ^ (c0 v c1)) = (((a0 v a1) ^ (c0 v c1)) ^ (b0 v b1))
366365lor 70 . . . . . . . . . . . 12 (b1 v (c2 ^ (c0 v c1))) = (b1 v (((a0 v a1) ^ (c0 v c1)) ^ (b0 v b1)))
367 leor 159 . . . . . . . . . . . . 13 b1 =< (b0 v b1)
368367ml2i 1123 . . . . . . . . . . . 12 (b1 v (((a0 v a1) ^ (c0 v c1)) ^ (b0 v b1))) = ((b1 v ((a0 v a1) ^ (c0 v c1))) ^ (b0 v b1))
369 ancom 74 . . . . . . . . . . . 12 ((b1 v ((a0 v a1) ^ (c0 v c1))) ^ (b0 v b1)) = ((b0 v b1) ^ (b1 v ((a0 v a1) ^ (c0 v c1))))
370366, 368, 3693tr 65 . . . . . . . . . . 11 (b1 v (c2 ^ (c0 v c1))) = ((b0 v b1) ^ (b1 v ((a0 v a1) ^ (c0 v c1))))
371370lan 77 . . . . . . . . . 10 (b0 ^ (b1 v (c2 ^ (c0 v c1)))) = (b0 ^ ((b0 v b1) ^ (b1 v ((a0 v a1) ^ (c0 v c1)))))
372 anass 76 . . . . . . . . . . 11 ((b0 ^ (b0 v b1)) ^ (b1 v ((a0 v a1) ^ (c0 v c1)))) = (b0 ^ ((b0 v b1) ^ (b1 v ((a0 v a1) ^ (c0 v c1)))))
373372cm 61 . . . . . . . . . 10 (b0 ^ ((b0 v b1) ^ (b1 v ((a0 v a1) ^ (c0 v c1))))) = ((b0 ^ (b0 v b1)) ^ (b1 v ((a0 v a1) ^ (c0 v c1))))
374 anabs 121 . . . . . . . . . . 11 (b0 ^ (b0 v b1)) = b0
375374ran 78 . . . . . . . . . 10 ((b0 ^ (b0 v b1)) ^ (b1 v ((a0 v a1) ^ (c0 v c1)))) = (b0 ^ (b1 v ((a0 v a1) ^ (c0 v c1))))
376371, 373, 3753tr 65 . . . . . . . . 9 (b0 ^ (b1 v (c2 ^ (c0 v c1)))) = (b0 ^ (b1 v ((a0 v a1) ^ (c0 v c1))))
377362, 376tr 62 . . . . . . . 8 (b0 ^ (((a0 ^ b0) v b1) v (c2 ^ (c0 v c1)))) = (b0 ^ (b1 v ((a0 v a1) ^ (c0 v c1))))
378377cm 61 . . . . . . 7 (b0 ^ (b1 v ((a0 v a1) ^ (c0 v c1)))) = (b0 ^ (((a0 ^ b0) v b1) v (c2 ^ (c0 v c1))))
379343, 378lbtr 139 . . . . . 6 (b0 ^ (a0 v p0)) =< (b0 ^ (((a0 ^ b0) v b1) v (c2 ^ (c0 v c1))))
380 orass 75 . . . . . . . . . 10 (((a0 ^ b0) v b1) v (c2 ^ (c0 v c1))) = ((a0 ^ b0) v (b1 v (c2 ^ (c0 v c1))))
381 orcom 73 . . . . . . . . . 10 ((a0 ^ b0) v (b1 v (c2 ^ (c0 v c1)))) = ((b1 v (c2 ^ (c0 v c1))) v (a0 ^ b0))
382380, 381tr 62 . . . . . . . . 9 (((a0 ^ b0) v b1) v (c2 ^ (c0 v c1))) = ((b1 v (c2 ^ (c0 v c1))) v (a0 ^ b0))
383382lan 77 . . . . . . . 8 (b0 ^ (((a0 ^ b0) v b1) v (c2 ^ (c0 v c1)))) = (b0 ^ ((b1 v (c2 ^ (c0 v c1))) v (a0 ^ b0)))
384 lear 161 . . . . . . . . 9 (a0 ^ b0) =< b0
385384mldual2i 1125 . . . . . . . 8 (b0 ^ ((b1 v (c2 ^ (c0 v c1))) v (a0 ^ b0))) = ((b0 ^ (b1 v (c2 ^ (c0 v c1)))) v (a0 ^ b0))
386 orcom 73 . . . . . . . 8 ((b0 ^ (b1 v (c2 ^ (c0 v c1)))) v (a0 ^ b0)) = ((a0 ^ b0) v (b0 ^ (b1 v (c2 ^ (c0 v c1)))))
387383, 385, 3863tr 65 . . . . . . 7 (b0 ^ (((a0 ^ b0) v b1) v (c2 ^ (c0 v c1)))) = ((a0 ^ b0) v (b0 ^ (b1 v (c2 ^ (c0 v c1)))))
388 lea 160 . . . . . . . 8 (a0 ^ b0) =< a0
389388leror 152 . . . . . . 7 ((a0 ^ b0) v (b0 ^ (b1 v (c2 ^ (c0 v c1))))) =< (a0 v (b0 ^ (b1 v (c2 ^ (c0 v c1)))))
390387, 389bltr 138 . . . . . 6 (b0 ^ (((a0 ^ b0) v b1) v (c2 ^ (c0 v c1)))) =< (a0 v (b0 ^ (b1 v (c2 ^ (c0 v c1)))))
391379, 390letr 137 . . . . 5 (b0 ^ (a0 v p0)) =< (a0 v (b0 ^ (b1 v (c2 ^ (c0 v c1)))))
392391df-le2 131 . . . 4 ((b0 ^ (a0 v p0)) v (a0 v (b0 ^ (b1 v (c2 ^ (c0 v c1)))))) = (a0 v (b0 ^ (b1 v (c2 ^ (c0 v c1)))))
39323, 392lbtr 139 . . 3 p =< (a0 v (b0 ^ (b1 v (c2 ^ (c0 v c1)))))
3942, 393lel2or 170 . 2 (a0 v p) =< (a0 v (b0 ^ (b1 v (c2 ^ (c0 v c1)))))
3951, 394letr 137 1 p =< (a0 v (b0 ^ (b1 v (c2 ^ (c0 v c1)))))
Colors of variables: term
Syntax hints:   = wb 1   =< wle 2   v wo 6   ^ wa 7  1wt 8
This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a4 33  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38  ax-ml 1120  ax-arg 1151
This theorem depends on definitions:  df-a 40  df-t 41  df-f 42  df-le1 130  df-le2 131
  Copyright terms: Public domain W3C validator