>(1R)-       /Symbols allowed.
sent          /Parameter categories allowed.
mp    /First rule is mp (modus ponens).
P     /It says that from P
P>Q   /and P->Q
:Q    /you can infer Q.
ti                           /Everything else in the file is an axiom.  The next
:p>(q>p)                /three axioms are tautologies from which all other
id                           /tautologies can be derived by modus ponens.  They
:(p>q>r)>(p>q)>(p>r)    /are not really needed since I have also included
con                          /the axiom...
:(-p>-q)>(-p>q)>p