loolin Show Code edit
## Lukasiewicz's Linearity Axiom
##
## The Linearity Axiom of the infinite-valued sentential logic (L-infinity)
## of Lukasiewicz.
##
thm (loolin () () (-> (-> (-> ph ps) (-> ps ph)) (-> ps ph))
ph ps (-> ps ph) himp1 pm2.43d)
(-> (-> (-> ph ps) (-> ps ph)) (-> ps ph))
edit