mpclosed

Theorem. Closed form of modus ponens.

Description:

Theorem *2.27 in Principia Mathematica; pm2.27 in set.mm. Also called "Assertion".

Arguments:

(pr), (pr),

Assertions:

((()))

Proof:

Hyp	Ref	Line	Expr
	id	1	(()())
1	com12i	2	((()))