ax5

Axiom.

Arguments:

x (sv), phi (pr), psi (pr),

Assertions:

(forallx(forallxphitopsi)to(forallxphitoforallxpsi))