Proving The Law of Introduction of Conjunction

The law sounds like: p implies that q implies that p and q. And the task is to prove that using just two first axioms of PL plus the Novikov's axiom (p⊃q)⊃((p⊃r)⊃(p⊃q&r)), that means that any formulations you can achieve by deriving them from p, you can conjunct them together, we can get the given formula. 

Γ,(p⊃q)⊃((p⊃r)⊃(p⊃q&r))⊢(p⊃(q⊃p&q))

Axoims:

(i) p⊃(q⊃p)
(ii) (p⊃(q⊃r))⊃((p⊃q)⊃(p⊃r))
(iii) (p⊃q)⊃((p⊃r)⊃(p⊃q&r))

1. (q⊃p)⊃((q⊃q)⊃(q⊃p&q)) /scheme A3/
2. (q⊃p)⊃((q⊃q)⊃(q⊃p&q))⊃((p⊃((q⊃p)⊃((q⊃q)⊃(q⊃p&q))) /scheme A1/
3. p⊃((q⊃p)⊃((q⊃q)⊃(q⊃p&q)) /1, 2 MP/
4. p⊃((q⊃p)⊃((q⊃q)⊃(q⊃p&q))⊃(p⊃(q⊃p))⊃(p⊃((q⊃q)⊃(q⊃p&q))) /scheme A2/
5. p⊃(q⊃p)⊃(p⊃((q⊃q)⊃(q⊃p&q)) /3, 4 MP/
6. p⊃(q⊃p) /sheme A1/
7. p⊃((q⊃q)⊃(q⊃p&q)) /5, 6 MP/
8. p⊃((q⊃q)⊃(q⊃p&q))⊃((p⊃(q⊃q))⊃(p⊃(q⊃p&q)) /scheme A2/
9. (p⊃(q⊃q))⊃(p⊃(q⊃p&q)) /7, 8 MP/
10. (p⊃(q⊃q))⊃(p⊃(q⊃p&q))⊃((q⊃q)⊃((p⊃(q⊃q))⊃(p⊃(q⊃p&q)) /scheme A1/
11. (q⊃q)⊃((p⊃(q⊃q))⊃(p⊃(q⊃p&q)) /9, 10 MP/
12. (q⊃q)⊃((p⊃(q⊃q))⊃(p⊃(q⊃p&q))⊃((q⊃q)⊃((p⊃(q⊃q))⊃((q⊃q))⊃(p⊃(q⊃p&q))) /scheme A2/
13. (q⊃q)⊃((p⊃(q⊃q))⊃((q⊃q))⊃(p⊃(q⊃p&q)) /11, 12 MP/
14. (q⊃q)⊃((p⊃(q⊃q)) /scheme A1/
15. (q⊃q)⊃(p⊃(q⊃p&q)) /13, 14 MP/
16. q⊃((q⊃q)⊃q) /scheme A1/
17. q⊃((q⊃q)⊃q)⊃((q⊃(q⊃q))⊃(q⊃q)) /scheme A2/
18. (q⊃(q⊃q))⊃(q⊃q)) /16, 17 MP/
19. q⊃(q⊃q) /scheme A1/
20. q⊃q /19, 18 MP/
     p⊃(q⊃p&q)) /21, 15 MP/

Hence, this proves that in the previous proof of the law of transportation instead of this axiom the Novikov's axiom may be used, that means that both of ways to prove the law of transportation is possible.