3jca Show Code edit
# Join consequents with conjunction.
thm (3jca () (3jca.1 (-> ph ps) 3jca.2 (-> ph ch) 3jca.3 (-> ph th)) (-> ph (/\/\ ps ch th)) 3jca.1 3jca.2 jca 3jca.3 jca ps ch th df-3an sylibr)
(-> ph (/\/\ ps ch th))
edit