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