notbii Show Code edit
## Negation Both Sides
##
## (<-> [ ph ] [ ps ] )
## (<-> (-. [ ph ] ) (-. [ ps ] ))
##
thm (notbii () (1 (<-> ph ps)) (<-> (-. ph) (-. ps))
1 biimpri con3i
(-> (-. ph) (-. ps))
1 biimpi con3i
(-> (-. ps) (-. ph))
impbii)
(<-> (-. ph) (-. ps))
edit