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