This brief manual assumes that you have read the help page for Truth Table and Fitch, Propositional in Proofmood.
In what follows, the expression φ(x) does not imply that x occurs in φ as a free variable, nor φ has no free variable other than x. We use the expression φ(t) to denote the formula that is obtained by substituting each free occurrence of x in φ(x) by t. (Provided that the substitution condition is met, of course.) In case there is no free occurrence of x in φ, φ(t) is identical to φ(x).
intro  elim  
∀ 
c is a fresh constant, x is a fresh individual variable. We may use ∀y φ(y) in place of ∀x φ(x). 
t is free to substitute x in φ 
∃ 
t is free to substitute x in φ 
c is a fresh constant and does not occur in θ. x is a fresh free variable and does not occur freely in θ. 
= 
t is a term. 
No variable occurring in t1,t2,s1,s2 cannot occur as a bound variable in α. 
TautConsq 
The conclusion is a tautological consequence of premises.
We may use subproofs as premises. 

Extended Rules  
intro  elim  
∀ 
We may use x1,x2 in place of c1,c2,
and ∀x2∀x1 in place of ∀x1∀x2.  
∃ 
We may use x1,x2(or y1,y2) in place of c1,c2, and ∃x2∃x1 in place of ∃x1∃x2. 

= elim 
Symmetricity = elim for identity
Transitivity
 
∀= elim 
We may use ∀x1∀x2(t(x1,x2)=s(x1,x2)) in place of t(x1,x2)=s(x1,x2) as a premise of [= elim] inference.
In this case, Proofmood behaves as if the premise t(r1,r2)=s(r1,r2) exists for some suitable terms r1 and r2. For transitivity, we may use such a universal formula for the last premise only.  
∀→ 
We may use {c1,c2} etc. in place of {c}.
We use the menu [∀ intro] for this extended rule of inference. 
We may use ∀x1∀x2 etc. in place of ∀x.
We use the menu [∀ elim] for this extended rule of inference. 
Associative 
An equation that can be obtained by applying the associativity ∀x∀y∀z(x·y·z = x·(y·z)) and [= elim]
several times, e.g., a·(b·c)·(d·e) = a·(b·(c·d))·e can be obtained by applying this rule of inference only once. The associativity axiom ∀x∀y∀z(x·y·z = x·(y·z)) should exist as a premise.  
Lemmas 
In the 6 formulas related to dummy, antecedent and consequent, x does not appear in β freely.
 
EquivRepl 
Line 10, the conclusion is obtained from the last premise(line 9) by replacing suitably chosen terms and subformulas in line 9 by terms and formulas designated as equivalent by the other premises(line 6,7,8). The substitution condition must be met of course. 

MetaSubst 
Substitute the formula φ(z), where a metasymbol φ occurs, with some other formula.
If there exists
a free variable of the substituting formula (¬(z=z)) which is not a free variable of φ,it must appear in the consequence formula (line 4) as a free variable.  