bitr3i Show Code edit
## Transitive Property
##
## (<-> ps ] [ ph ] )
## (<-> ps ] [ [ ch)
## (<-> [ [ ph [ ch)
##
thm (bitr3i () (1 (<-> ps ph) 2 (<-> ps ch)) (<-> ph ch)
1 bicomi 2 bitri)
(<-> ph ch)
edit