anmp<>

Theorem.

Arguments:

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

Hypotheses:

((phiwedgepsi)tochi)
psi
phi

Assertions:

chi

Proof:

Hyp Ref Line Expr
Hypo1((phiwedgepsi)tochi)
2psi
3phi
2, 3>andi4(phiwedgepsi)
1, 4ax-mp5chi