2false Show Code edit
## Two falsehoods are equivalent
thm (2false () (2false.1 (-. ph) 2false.2 (-. ps)) (<-> ph ps) 2false.1 2false.2 ph ps pm5.21 mp2an)
(<-> ph ps)
edit