2th Show Code edit
## Two truths are equivalent
thm (2th () (2th.1 ph 2th.2 ps) (<-> ph ps) 2th.2 ph a1i 2th.1 ps a1i impbii)
(<-> ph ps)
edit