ax4

Axiom.

Arguments:

x (sv), phi (pr),

Assertions:

(forallxphitophi)