ancomsd

Theorem.

Arguments:

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

Hypotheses:

(phito((psiwedgechi)totheta))

Assertions:

(phito((chiwedgepsi)totheta))

Proof:

Hyp Ref Line Expr
Hypo1(phito((psiwedgechi)totheta))
ancom2((chiwedgepsi)leftrightarrow(psiwedgechi))
1, 2brpi323(phito((chiwedgepsi)totheta))