Quantum Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  QLE Home  >  Th. List  >  u3lemax5 GIF version

Theorem u3lemax5 797
 Description: Possible axiom for Kalmbach implication system.
Assertion
Ref Expression
u3lemax5 ((a3 b) →3 ((a3 b) →3 ((b3 a) →3 ((b3 a) →3 ((b3 c) →3 ((b3 c) →3 ((c3 b) →3 ((c3 b) →3 (a3 c))))))))) = 1

Proof of Theorem u3lemax5
StepHypRef Expression
1 lem4 511 . 2 ((a3 b) →3 ((a3 b) →3 ((b3 a) →3 ((b3 a) →3 ((b3 c) →3 ((b3 c) →3 ((c3 b) →3 ((c3 b) →3 (a3 c))))))))) = ((a3 b) ∪ ((b3 a) →3 ((b3 a) →3 ((b3 c) →3 ((b3 c) →3 ((c3 b) →3 ((c3 b) →3 (a3 c))))))))
2 lem4 511 . . . . 5 ((b3 a) →3 ((b3 a) →3 ((b3 c) →3 ((b3 c) →3 ((c3 b) →3 ((c3 b) →3 (a3 c))))))) = ((b3 a) ∪ ((b3 c) →3 ((b3 c) →3 ((c3 b) →3 ((c3 b) →3 (a3 c))))))
3 lem4 511 . . . . . . 7 ((b3 c) →3 ((b3 c) →3 ((c3 b) →3 ((c3 b) →3 (a3 c))))) = ((b3 c) ∪ ((c3 b) →3 ((c3 b) →3 (a3 c))))
4 lem4 511 . . . . . . . . 9 ((c3 b) →3 ((c3 b) →3 (a3 c))) = ((c3 b) ∪ (a3 c))
54lor 70 . . . . . . . 8 ((b3 c) ∪ ((c3 b) →3 ((c3 b) →3 (a3 c)))) = ((b3 c) ∪ ((c3 b) ∪ (a3 c)))
6 ax-a3 32 . . . . . . . . . 10 (((b3 c) ∪ (c3 b) ) ∪ (a3 c)) = ((b3 c) ∪ ((c3 b) ∪ (a3 c)))
76ax-r1 35 . . . . . . . . 9 ((b3 c) ∪ ((c3 b) ∪ (a3 c))) = (((b3 c) ∪ (c3 b) ) ∪ (a3 c))
8 oran3 93 . . . . . . . . . . 11 ((b3 c) ∪ (c3 b) ) = ((b3 c) ∩ (c3 b))
9 u3lembi 723 . . . . . . . . . . . 12 ((b3 c) ∩ (c3 b)) = (bc)
109ax-r4 37 . . . . . . . . . . 11 ((b3 c) ∩ (c3 b)) = (bc)
118, 10ax-r2 36 . . . . . . . . . 10 ((b3 c) ∪ (c3 b) ) = (bc)
1211ax-r5 38 . . . . . . . . 9 (((b3 c) ∪ (c3 b) ) ∪ (a3 c)) = ((bc) ∪ (a3 c))
137, 12ax-r2 36 . . . . . . . 8 ((b3 c) ∪ ((c3 b) ∪ (a3 c))) = ((bc) ∪ (a3 c))
145, 13ax-r2 36 . . . . . . 7 ((b3 c) ∪ ((c3 b) →3 ((c3 b) →3 (a3 c)))) = ((bc) ∪ (a3 c))
153, 14ax-r2 36 . . . . . 6 ((b3 c) →3 ((b3 c) →3 ((c3 b) →3 ((c3 b) →3 (a3 c))))) = ((bc) ∪ (a3 c))
1615lor 70 . . . . 5 ((b3 a) ∪ ((b3 c) →3 ((b3 c) →3 ((c3 b) →3 ((c3 b) →3 (a3 c)))))) = ((b3 a) ∪ ((bc) ∪ (a3 c)))
172, 16ax-r2 36 . . . 4 ((b3 a) →3 ((b3 a) →3 ((b3 c) →3 ((b3 c) →3 ((c3 b) →3 ((c3 b) →3 (a3 c))))))) = ((b3 a) ∪ ((bc) ∪ (a3 c)))
1817lor 70 . . 3 ((a3 b) ∪ ((b3 a) →3 ((b3 a) →3 ((b3 c) →3 ((b3 c) →3 ((c3 b) →3 ((c3 b) →3 (a3 c)))))))) = ((a3 b) ∪ ((b3 a) ∪ ((bc) ∪ (a3 c))))
19 ax-a3 32 . . . . 5 (((a3 b) ∪ (b3 a) ) ∪ ((bc) ∪ (a3 c))) = ((a3 b) ∪ ((b3 a) ∪ ((bc) ∪ (a3 c))))
2019ax-r1 35 . . . 4 ((a3 b) ∪ ((b3 a) ∪ ((bc) ∪ (a3 c)))) = (((a3 b) ∪ (b3 a) ) ∪ ((bc) ∪ (a3 c)))
21 oran3 93 . . . . . . 7 ((a3 b) ∪ (b3 a) ) = ((a3 b) ∩ (b3 a))
22 u3lembi 723 . . . . . . . 8 ((a3 b) ∩ (b3 a)) = (ab)
2322ax-r4 37 . . . . . . 7 ((a3 b) ∩ (b3 a)) = (ab)
2421, 23ax-r2 36 . . . . . 6 ((a3 b) ∪ (b3 a) ) = (ab)
2524ax-r5 38 . . . . 5 (((a3 b) ∪ (b3 a) ) ∪ ((bc) ∪ (a3 c))) = ((ab) ∪ ((bc) ∪ (a3 c)))
26 le1 146 . . . . . 6 ((ab) ∪ ((bc) ∪ (a3 c))) ≤ 1
27 ska2 432 . . . . . . . 8 ((ab) ∪ ((bc) ∪ (ac))) = 1
2827ax-r1 35 . . . . . . 7 1 = ((ab) ∪ ((bc) ∪ (ac)))
29 u3lembi 723 . . . . . . . . . . 11 ((a3 c) ∩ (c3 a)) = (ac)
3029ax-r1 35 . . . . . . . . . 10 (ac) = ((a3 c) ∩ (c3 a))
31 lea 160 . . . . . . . . . 10 ((a3 c) ∩ (c3 a)) ≤ (a3 c)
3230, 31bltr 138 . . . . . . . . 9 (ac) ≤ (a3 c)
3332lelor 166 . . . . . . . 8 ((bc) ∪ (ac)) ≤ ((bc) ∪ (a3 c))
3433lelor 166 . . . . . . 7 ((ab) ∪ ((bc) ∪ (ac))) ≤ ((ab) ∪ ((bc) ∪ (a3 c)))
3528, 34bltr 138 . . . . . 6 1 ≤ ((ab) ∪ ((bc) ∪ (a3 c)))
3626, 35lebi 145 . . . . 5 ((ab) ∪ ((bc) ∪ (a3 c))) = 1
3725, 36ax-r2 36 . . . 4 (((a3 b) ∪ (b3 a) ) ∪ ((bc) ∪ (a3 c))) = 1
3820, 37ax-r2 36 . . 3 ((a3 b) ∪ ((b3 a) ∪ ((bc) ∪ (a3 c)))) = 1
3918, 38ax-r2 36 . 2 ((a3 b) ∪ ((b3 a) →3 ((b3 a) →3 ((b3 c) →3 ((b3 c) →3 ((c3 b) →3 ((c3 b) →3 (a3 c)))))))) = 1
401, 39ax-r2 36 1 ((a3 b) →3 ((a3 b) →3 ((b3 a) →3 ((b3 a) →3 ((b3 c) →3 ((b3 c) →3 ((c3 b) →3 ((c3 b) →3 (a3 c))))))))) = 1
 Colors of variables: term Syntax hints:   = wb 1  ⊥ wn 4   ≡ tb 5   ∪ wo 6   ∩ wa 7  1wt 8   →3 wi3 14 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-wom 361  ax-r3 439 This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i1 44  df-i2 45  df-i3 46  df-le 129  df-le1 130  df-le2 131  df-c1 132  df-c2 133  df-cmtr 134 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator