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

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

Proof of Theorem u3lemax4
StepHypRef Expression
1 lem4 511 . 2 ((a3 b) →3 ((a3 b) →3 ((b3 a) →3 ((b3 a) →3 ((c3 (c3 a)) →3 (c3 (c3 b))))))) = ((a3 b) ∪ ((b3 a) →3 ((b3 a) →3 ((c3 (c3 a)) →3 (c3 (c3 b))))))
2 lem4 511 . . . . 5 ((b3 a) →3 ((b3 a) →3 ((c3 (c3 a)) →3 (c3 (c3 b))))) = ((b3 a) ∪ ((c3 (c3 a)) →3 (c3 (c3 b))))
3 lem4 511 . . . . . . 7 (c3 (c3 a)) = (ca)
4 lem4 511 . . . . . . 7 (c3 (c3 b)) = (cb)
53, 42i3 254 . . . . . 6 ((c3 (c3 a)) →3 (c3 (c3 b))) = ((ca) →3 (cb))
65lor 70 . . . . 5 ((b3 a) ∪ ((c3 (c3 a)) →3 (c3 (c3 b)))) = ((b3 a) ∪ ((ca) →3 (cb)))
72, 6ax-r2 36 . . . 4 ((b3 a) →3 ((b3 a) →3 ((c3 (c3 a)) →3 (c3 (c3 b))))) = ((b3 a) ∪ ((ca) →3 (cb)))
87lor 70 . . 3 ((a3 b) ∪ ((b3 a) →3 ((b3 a) →3 ((c3 (c3 a)) →3 (c3 (c3 b)))))) = ((a3 b) ∪ ((b3 a) ∪ ((ca) →3 (cb))))
9 oran3 93 . . . . . 6 ((a3 b) ∪ (b3 a) ) = ((a3 b) ∩ (b3 a))
10 u3lembi 723 . . . . . . 7 ((a3 b) ∩ (b3 a)) = (ab)
1110ax-r4 37 . . . . . 6 ((a3 b) ∩ (b3 a)) = (ab)
129, 11ax-r2 36 . . . . 5 ((a3 b) ∪ (b3 a) ) = (ab)
1312ax-r5 38 . . . 4 (((a3 b) ∪ (b3 a) ) ∪ ((ca) →3 (cb))) = ((ab) ∪ ((ca) →3 (cb)))
14 ax-a3 32 . . . 4 (((a3 b) ∪ (b3 a) ) ∪ ((ca) →3 (cb))) = ((a3 b) ∪ ((b3 a) ∪ ((ca) →3 (cb))))
15 le1 146 . . . . 5 ((ab) ∪ ((ca) →3 (cb))) ≤ 1
16 ska4 433 . . . . . . . 8 ((ab ) ∪ ((ac) ≡ (bc))) = 1
1716ax-r1 35 . . . . . . 7 1 = ((ab ) ∪ ((ac) ≡ (bc)))
18 conb 122 . . . . . . . . . 10 (ab) = (ab )
1918ax-r4 37 . . . . . . . . 9 (ab) = (ab )
20 conb 122 . . . . . . . . . 10 ((ca) ≡ (cb)) = ((ca) ≡ (cb) )
21 ancom 74 . . . . . . . . . . . . 13 (ac) = (ca )
22 anor1 88 . . . . . . . . . . . . 13 (ca ) = (ca)
2321, 22ax-r2 36 . . . . . . . . . . . 12 (ac) = (ca)
24 ancom 74 . . . . . . . . . . . . 13 (bc) = (cb )
25 anor1 88 . . . . . . . . . . . . 13 (cb ) = (cb)
2624, 25ax-r2 36 . . . . . . . . . . . 12 (bc) = (cb)
2723, 262bi 99 . . . . . . . . . . 11 ((ac) ≡ (bc)) = ((ca) ≡ (cb) )
2827ax-r1 35 . . . . . . . . . 10 ((ca) ≡ (cb) ) = ((ac) ≡ (bc))
2920, 28ax-r2 36 . . . . . . . . 9 ((ca) ≡ (cb)) = ((ac) ≡ (bc))
3019, 292or 72 . . . . . . . 8 ((ab) ∪ ((ca) ≡ (cb))) = ((ab ) ∪ ((ac) ≡ (bc)))
3130ax-r1 35 . . . . . . 7 ((ab ) ∪ ((ac) ≡ (bc))) = ((ab) ∪ ((ca) ≡ (cb)))
3217, 31ax-r2 36 . . . . . 6 1 = ((ab) ∪ ((ca) ≡ (cb)))
33 u3lembi 723 . . . . . . . . 9 (((ca) →3 (cb)) ∩ ((cb) →3 (ca))) = ((ca) ≡ (cb))
3433ax-r1 35 . . . . . . . 8 ((ca) ≡ (cb)) = (((ca) →3 (cb)) ∩ ((cb) →3 (ca)))
35 lea 160 . . . . . . . 8 (((ca) →3 (cb)) ∩ ((cb) →3 (ca))) ≤ ((ca) →3 (cb))
3634, 35bltr 138 . . . . . . 7 ((ca) ≡ (cb)) ≤ ((ca) →3 (cb))
3736lelor 166 . . . . . 6 ((ab) ∪ ((ca) ≡ (cb))) ≤ ((ab) ∪ ((ca) →3 (cb)))
3832, 37bltr 138 . . . . 5 1 ≤ ((ab) ∪ ((ca) →3 (cb)))
3915, 38lebi 145 . . . 4 ((ab) ∪ ((ca) →3 (cb))) = 1
4013, 14, 393tr2 64 . . 3 ((a3 b) ∪ ((b3 a) ∪ ((ca) →3 (cb)))) = 1
418, 40ax-r2 36 . 2 ((a3 b) ∪ ((b3 a) →3 ((b3 a) →3 ((c3 (c3 a)) →3 (c3 (c3 b)))))) = 1
421, 41ax-r2 36 1 ((a3 b) →3 ((a3 b) →3 ((b3 a) →3 ((b3 a) →3 ((c3 (c3 a)) →3 (c3 (c3 b))))))) = 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