>(1R)~(1R)^(2L)v(2L)-AE    /Symbols allowed
pred, func, const   /Parameter categories allowed.  (Could allow sent too?)
mp    /First rule is mp (modus ponens).
P     /It says that from P
P>Q   /and P->Q
:Q    /you can infer Q.
ui
P[x*]>Q
:P>AxQ
ei
P>Q[x*]
:ExP>Q
a1.
:P>(Q>P)
a2.
:(P>(Q>R))>((P>Q)>(P>R))
a3.
:P>(Q>(P^Q))
a4.
:(P^Q)>P
a5.
:(P^Q)>Q
a6.
:P>(PvQ)
a7.
:Q>(PvQ)
a8.
:(P>R)>((Q>R)>((PvQ)>R))
a9.
:--P~P
a10.
:-(PvQ)~(-P^-Q)
a11.
:-(P^Q)~(-Pv-Q)
a12.
:-(P>Q)~(P>-Q)
a13.
:-ExP~Ax-P
a14.
:-AxP~Ex-P
a15.
:P[x|a]>ExP
a16.
:AxP>P[x|a]