bneg>

Theorem.

Arguments:

phi (pr),

Assertions:

(phileftrightarrowlnotlnotphi)

Proof:

Hyp Ref Line Expr
neg>1(phitolnotlnotphi)
neg<2(lnotlnotphitophi)
1, 2>bii3(phileftrightarrowlnotlnotphi)