casei

Theorem.

Arguments:

phi (pr), psi (pr),

Hypotheses:

(lnotphitopsi)
(phitopsi)

Assertions:

psi

Proof:

Hyp Ref Line Expr
Hypo1(lnotphitopsi)
2(phitopsi)
case3((phitopsi)to((lnotphitopsi)topsi))
2, 3ax-mp4((lnotphitopsi)topsi)
1, 4ax-mp5psi