Is there a general procedure to generate theorems from axioms by hand? I am checking a book of Jan Łukasiewicz "Elements of Mathmatical Logic".
In one section of the book (from page 42 I think), he worked around an axiom system like this one:
Axiom system of $L$: 
(B1) $(\lnot B \rightarrow B) \rightarrow B$ 
(B2) $B \rightarrow (\lnot B \rightarrow C)$ 
(B3) $(B \rightarrow C) \rightarrow ((C \rightarrow D) \rightarrow (B \rightarrow D))$ 
the only rule of inference is modus ponens.
Then , like magic , he derived over 50 theorems from them(I can't even finish reading them)! I saw he used a technique like this:
Choose a thesis $\to$ substitute letters $\to$ left one is a thesis $\to$ right one is a new thesis (by MP)
The tricky part is substitution (for me).How did he(Jan Łukasiewicz) substitute just the right wf for the letters so that the left one becomes a thesis.Or did he checked all the substitution by hand? How long did it take him to do something like this?
 A: I remember a similar sort of amazement with Lukasiewcz when first reading that text.  I can't answer all of your questions.  I have other ones like "how did he have the confidence that his preferred three axiom set would work in the first place?"
No, there is not a general procedure to generate theorems from axioms by hand.
Suppose that there existed some general procedure.  Then, for all axioms we could generate at least one theorem.  But, consider the axiom CCNppp and suppose that is the only axiom we have.  We'll need to find two theorems of the type CCNppp in order to detach a theorem, since we can only use the rule of detachment, and the only theorem we know of is CCNppp.  One will have form C$\alpha$$\beta$, which can get called the major premise, and the other $\alpha$, which can get called the minor premise.  But, since C$\alpha$$\beta$ has the type CCNppp, this implies that $\alpha$ has the type CNpp also.  Any formula of the type CCNppp does not have a negation symbol in the second position, and cannot since substitution never produces a shorter meaningful expression than we started with.
We could also consider a system with the axioms CCpqCCqrCpr, CpCNpq, and CCNppp where CCNppp is always the major premise.  But then CCpqCCqrCpr and CpCNpq would have to have the type CNpp.  They don't since the second symbol of CCpqCCqrCpr is not an 'N', nor a variable, and because the consequent of meaningful expressions of the type CpCNpq is longer than the antecedent, while the antecedent of meaningful expressions of the type CNpp is longer than the consequent, and all substitutions for the meaningful expressions CpCNpq and CNpp preserve the relationship in length between the antecedent and consequent of the meaningful expressions.  That relationship gets preserved for CNpp since substitution is uniformly applied across a meaningful expression to all similar symbols of the same type, and for CpCNpq by a similar argument while also noting that any substitution in the consequent will preserve the property of the antecedent being shorter than the consequent.
Given that we've proved soundness, we could also argue that since CNpp is not a tautology, it is not possible to ever use CCNppp as a major premise.
How did Lukasiewicz find his substitutions?  I don't know.  My recollection of trying to redo the substitutions is that I found two mistakes.  Lukasiewicz does not also always find the most general possible theorem derivable from the axiom(s)/theorem(s) he uses when making a detachment.  What I do know is that in J. J. Zeman's book Modal logic: The Lewis-modal systems, in the introduction he uses diagrammatic techniques which the writing suggests to me that he got from A. N. Prior, and Prior collaborated with Meredith who studied with Lukasiewicz.
As an example, let's say we define a new system with the following formation rules.

*

*'0' is a meaningful expression which is a constant.

*The numerals '3' through '9' are meaningful expressions.

*If 'x' is a meaningful expression, then '1x' is a meaningful expression.

*If 'x' and 'y' are meaningful expressions, then '2xy' is a meaningful expression.

*Nothing else is a meaningful expression in this language.

Suppose we have 2223403 as thesis, with the rule of inference '2xy' and 'x' as theses, allows us to detach 'y' as a thesis.  Can we derive anything from 2223403?  We can at least substitute numerals for '3' and '4' such that we'll have two meaningful expressions of the type 2228908 such that both of the expressions do not have any numerals in common which succeed '2' in the numeral sequence '0', '1', '2', '3', '4', '5', '6', '7', '8', '9'.  2223403 and 2225605 are two such expressions.
Here's a diagram which helps to find a substitution, I think.
2 2 2 3     4 0 3
  | | |     | -
  | | ----- - |
  2 2 2 5 6 0 5

Here we have a type to guide finding the major premise above the minor premise.  Thus, we need to find some form which matches or unifies 22340 with 2225605.
A collection of symbols like
|
-

suggests a relationship where some sub-expression in the upper expression gets substituted with something in the lower expression.
A collection of symbols like
-
|

suggests a relations where some sub-expression the lower expression gets substituted with something in the upper expression.
Substitutions getting applied to the shortest sub-expressions first, I think, makes for a good general rule.  In the above, due to left-to-right reading, I suppose, it might feel useful to substitution '3' in the upper with '256' in the lower.  But, '5' is in '256' and appears later in 2225605.  So, it makes more sense to apply substitutions for the shortest meaningful expressions first.
Thus, we substitute '4' with '0', and '5' with '0'.  And '3' with '206', since the '5' in '256' needed substituted with '0'.
So, the major premise we find from 2223403 is 22220600206, and the minor premise from 2223403 is not 2225606, but instead 2220600.  Thus, we can detach 206.  I'll note that 2223403 can get interpreted as meaning "if an arbitrary conditional implies a constant false proposition, then it's antecedent is true" and 206 can get interpreted as meaning "if a constant false proposition, then any proposition follows."
I suggest that to find a thesis from two theses, you first make sure that the theses you will use to find a derivation have completely distinct variables.  Then, try to make diagrams as above as aids and use as little substitution as possible.
