question about translating to logical connectives

Hi Everyone,

This is my first time using the forum mailing list. Hope to learn to use it well! If there is a guidance of sort of questions that are appropriate feel free to share it with me, Especially for really basic questions? :)

I was trying to do exercise exercise 1.3.1 of https://www.cs.ru.nl/~freek/mizar/mizman.ps.gz 9 easy steps of Mizar. I tried translating

phi iff not not phi

and put it in mizar and mizar threw me some errors:

:: example of a comment
environ
  vocabularies MY_MIZAR;
begin
phi implies not not psi & not not psi implies phi;
::>*321
::>
::> 321: Predicate symbol or "is" expected

I put after the environ begin clause but throws an error that isn’t too helpful. How can I check if what I am doing in that exercise I am doing correctly?

Regards, Brando