mpd

Theorem. A modus ponens deduction.

Arguments:

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

Hypotheses:

(phito(psitochi))
(phitopsi)

Assertions:

(phitochi)

Proof:

Hyp Ref Line Expr
Hypo1(phito(psitochi))
2(phitopsi)
1ax23((phitopsi)to(phitochi))
2, 3ax-mp4(phitochi)