anmp<i

Theorem.

Arguments:

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

Hypotheses:

psi
(phito((psiwedgechi)totheta))

Assertions:

(phito(chitotheta))

Proof:

Hyp Ref Line Expr
Hypo1psi
2(phito((psiwedgechi)totheta))
2exp3a3(phito(psito(chitotheta)))
1, 3mpi4(phito(chitotheta))