BiReplaceImp0An1 Show Code edit
## Substitution
##
## (-> (/\ ph [ ps ] ] ] ) th)
## (<-> [ ps ] [ ch ] )
## (-> (/\ ph [ [ [ ch ] ) th)
##
thm (BiReplaceImp0An1 () (
replacee (-> (/\ ph ps) th)
substitution (<-> ps ch))
(-> (/\ ph ch) th)
replacee substitution
(<-> ps ch)
ph anbi2i
(<-> (/\ ph ps) (/\ ph ch))
sylbi2
(-> (/\ ph ch) th)
)
edit