# Is this Proof of (P→Q)→((Q→R)→(P→R)) based on Lukasiewicz Axiom System for CPL Correct?

Given Lukasiewicz axiom system for Classical Propositional Logic (CPL):

(L1) α→(β→α)

(L2) (α→(β→γ))→(α→β)→(α→γ)

(L3) (¬α→¬β)→(β→α)

and the usual Modus Ponens, does my proof of (P→Q)→((Q→R)→(P→R)) below correct? Can someone point out where I made mistake?

(1) (P→R)→((Q→R)→(P→R)) (L1)

(2) (P→(Q→R))→((P→Q)→(P→R)) (L2)

(3) (Q→R)→(P→(Q→R)) (L1)

(4) (P→Q)→(P→R) (2,3 MP)

(5) (Q→R)→(P→R) (1,4 MP)

(6) (P→Q)→((Q→R)→(P→R)) (4,5 MP)

• How does your step (4) work? The only deduction I can see from (2), (3) is the derived rule HS giving $(Q\to R)\to((P\to Q)\to(P\to R))$. – user10354138 May 22 at 5:27
• You can find the proof in the answer to this post : T2. – Mauro ALLEGRANZA May 22 at 6:15