jaoi Show Code edit
# Inference disjoining the antecedents of two implications.
## Join two implications
##
## (-> ph ] ] ] ps)
## (-> [ [ ch ] ps)
## (-> (\/ ph ] [ ch ] ) ps)
##
thm (jaoi () (jaoi.1 (-> ph ps) jaoi.2 (-> ch ps)) (-> (\/ ph ch) ps) jaoi.1 jaoi.2 ph ps ch jao mp2)
(-> (\/ ph ch) ps)
edit