biantru Show Code edit
# A wff is equivalent to its conjunction with truth.
thm (biantru () (biantru.1 ph) (<-> ps (/\ ps ph)) biantru.1 ph ps iba ax-mp)
(<-> ps (/\ ps ph))
edit