nic-bijust Show Code edit
# For nic-* definitions, the biconditional connective is not used. Instead,
# definitions are made based on this form. [[nic-bi1]] and [[nic-bi2]] are
# used to convert the definitions into usable theorems about one side of the
# implication. (Contributed by Jeff Hoffman, 18-Nov-2007.)
thm (nic-bijust () () (-/\ (-/\ ta ta) (-/\ (-/\ ta ta) (-/\ ta ta))) (-/\ ta ta) nic-id)
(-/\ (-/\ ta ta) (-/\ (-/\ ta ta) (-/\ ta ta)))
edit