anabs<

Theorem.

Arguments:

phi (pr), psi (pr),

Assertions:

((phiwedge(phiwedgepsi))leftrightarrow(phiwedgepsi))

Proof:

Hyp Ref Line Expr
ancom1((phiwedge(phiwedgepsi))leftrightarrow((phiwedgepsi)wedgephi))
<anabs<2(((phiwedgepsi)wedgephi)leftrightarrow(phiwedgepsi))
1, 2bitr3((phiwedge(phiwedgepsi))leftrightarrow(phiwedgepsi))