an23ass

Theorem.

Arguments:

phi (pr), psi (pr), chi (pr),

Assertions:

(((phiwedgepsi)wedgechi)leftrightarrow((phiwedgechi)wedgepsi))

Proof:

Hyp Ref Line Expr
ancom1((psiwedgechi)leftrightarrow(chiwedgepsi))
1bi.bldan>2((phiwedge(psiwedgechi))leftrightarrow(phiwedge(chiwedgepsi)))
anass3(((phiwedgepsi)wedgechi)leftrightarrow(phiwedge(psiwedgechi)))
anass4(((phiwedgechi)wedgepsi)leftrightarrow(phiwedge(chiwedgepsi)))
2, 3, 4<2bitr5(((phiwedgepsi)wedgechi)leftrightarrow((phiwedgechi)wedgepsi))