BiReplaceImp0Not0 Show Code edit
## Substitution
##
## (-> (-. [ ph ] ] ] ) ch)
## (<-> [ ph ] [ ps ] )
## (-> (-. [ [ [ ps ] ) ch)
##
thm (BiReplaceImp0Not0 () (
replacee (-> (-. ph) ch)
substitution (<-> ph ps))
(-> (-. ps) ch)
replacee substitution
(<-> ph ps)
con4biir
(<-> (-. ph) (-. ps))
sylbi2
(-> (-. ps) ch)
)
edit