anmp22

Theorem.

Arguments:

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

Hypotheses:

((phiwedge(psiwedgechi))totheta)
chi

Assertions:

((phiwedgepsi)totheta)

Proof:

Hyp Ref Line Expr
Hypo1((phiwedge(psiwedgechi))totheta)
2chi
1exp3(phito((psiwedgechi)totheta))
2, 3anmp>i4(phito(psitotheta))
4imp5((phiwedgepsi)totheta)