jca Show Code edit
## Join two implications
##
## (-> ph ps ] ] )
## (-> ph ] [ ch)
## (-> ph (/\ ps ] [ ch))
##
thm (jca () (jca.1 (-> ph ps) jca.2 (-> ph ch)) (-> ph (/\ ps ch)) jca.1 jca.2 jc ps ch df-an sylibr)
(-> ph (/\ ps ch))
edit