Here is a proof of Modus Ponens. This proof will use Polish Notation, relies on three axioms & one rule of inference. The proof for Modus Ponens will rely on 13 Lemmas. This axiomatic system only has two primitive logical operators, which is C and N, or Implication and Negation.

A quick note on notation.

C stands for implication, i.e. –>

N stand for negation, i.e. ~

Axiom 1: CCpqCCqrCpr [Hypothetical Syllogism]

Axiom 2: CCNppp [Clavis Law, i.e. Reductio Ad Absurdum]

Axiom 3: CpCNpq [Dun Scotus Law, i.e. Law of Denying Antecedent]

Inference Rule:

Rule of Detachment (MP): Φ & CΦΩ implies Ω

Lemma 4: CCCCqrCprsCCpqs

1. CCpqCCqrCpr [sub. p/Cpq, q/CCqrCpr, r/s in Axiom 1]

2. CCCpqCCqrCprCCCCqrCprsCCpqs

3. CCCCqrCprsCCpqs [(1)/(2) MP] Q.E.D.

Lemma 5: CCpCqrCCsqCpCsr

1. CCCCqrCprsCCpqs [sub. q/Cqr, r/Csr, s/CCsqCpCsr in L4]

2. CCCCCqrCsrCpCsrCCsqCpCsrCCpCqrCCsqCpCsr

3. CCCCqrCprsCCpqs [sub. p/s, s/CpCsr in L4]

4. CCCCCqrCsrCpCsrCCsqCpCsr

5. CCpCqrCCsqCpCsr [(2)/(4) MP] Q.E.D.

Lemma 6: CCpqCCCprsCCqrs

1. CCCCqrCprsCCpqs [sub. s/CCCprsCCqrs in L4]

2. CCCCqrCprCCCprsCCqrsCCpqCCCprsCCqrs

3. CCpqCCqrCpr [sub. p/Cqr, q/Cpr, r/s in Axiom 1]

4. CCCqrCprCCCprsCCqrs

5. CCpqCCCprsCCqrs [(2)/(4) MP] Q.E.D.

Lemma 7: CCtCCprsCCpqCtCCqrs

1. CCpCqrCCsqCpCsr [sub. p/Cpq, q/CCprs, r/CCqrs, s/t in L5]

2. CCCpqCCCprsCCqrsCCtCCprsCCpqCtCCqrs

3. CCtCCprsCCpqCtCCqrs [(2)/(L6) MP] Q.E.D.

Lemma 9: CCCNpqrCpr

1. CCpqCCqrCpr [sub. q/CNpq in Axiom 1]

2. CCpCNpqCCCNpqrCpr

3. CCCNpqrCpr [(2)/(Axiom 3) MP] Q.E.D.

Lemma 10: CpCCCNpppCCqpp

1. CCCNpqrCpr [sub. r/CCCNpppCCqpp in L9]

2. CCCNpqCCCNpppCCqppCpCCCNpppCCqpp

3. CCpqCCCprsCCqrs [sub. p/Np, r/p, s/p in L6]

4. CCNpqCCCNpppCCqpp

5. CpCCCNpppCqpp [(2)/(4) MP] Q.E.D.

Lemma 11: CCqCCNpppCCNppp

1. CpCCCNpppCCqpp [sub. p/CCNppp in L10]

2. CCCNpppCCCNpCCNpppCCNpppCCqCCNpppCCNppp

3. CCCNpCCNpppCCNpppCCqCCNpppCCNppp [(2)/(Axiom 2) MP]

4. CCNppp [sub. p/CCNppp in Axiom 2]

5. CCNpCCNpppCCNppp

6. CCqCCNpppCCNppp [(3)/(5) MP] Q.E.D.

Lemma 12: CtCCNppp

1. CCCNpqrCpr [sub. p/t, q/CCNppp, r/CCNppp in L9]]

2. CCCNtCCNpppCCNpppCtCCNppp

3. CCqCCNpppCCNppp [sub. q/Nt, in L11]

4. CCNtCCNpppCCNppp

5. CtCCNppp [(2)/(4) MP] Q.E.D.

Lemma 13: CCNpqCtCCqpp

1. CCtCCprsCCpqCtCCqrs [sub. p/Np, r/p, s/p in L7]

2. CCtCCNpppCCNpqCtCCtCCqpp

3. CCNpqCtCCqpp [(2)/(L12) MP] Q.E.D.

Lemma 14: CCCtCCqpprCCNpqr

1. CCpqCCqrCpr [sub. p/CNpq, q/CtCCqpp in Axiom 1]

2. CCCNpqCtCCqppCCCtCCqpprCNpqr

3. CCCtCCqpprCNpqr [(2)/(L13) MP] Q.E.D.

Lemma 15: CCNpqCCqpp

1. CCCtCCqpprCCNpqr [sub. t/NCCqpp, r/Cqpp in L14]

2. CCCNCCqppCCqppCCqppCCNpqCCqpp

3. CCNppp [sub. p/CCqpp in Axiom 2]

4. CCNCCqppCCqppCCqpp

5. CCNpqCCqpp [(2)/(4) MP] Q.E.D.

Lemma 17: CpCCqpp

1. CCCNpqrCpr [sub. r/CCqpp in L9]

2. CCCNpqCCqppCpCCqpp

3. CpCCqpp [(2)/(L15) MP] Q.E.D.

Lemma 18: CqCpq [Law of Affirming Consequent/Law of Simplification]

1. CCpCqrCCsqCpCsr [sub. p/q, q/CNpq, r/q, s/p in L5]

2. CCqCCNpqqCCpCNpqCqCpq

3. CpCCqpp [sub. p/q, q/Np in L17]

4. CqCCNpqq

5. CCpCNpqCqCpq [(2)/(4) MP]

6. CqCpq [(5)/(Axiom 3) MP] Q.E.D.

Lemma 19: CCCpqrCqr

1. CCpqCCqrCpr [sub. p/q, q/Cpq in Axiom 1]

2. CCqCpqCCCpqrCqr

3. CCCpqrCqr [(2)/(L18) MP] Q.E.D.

Modus Ponens: CpCCpqq

1. CCCpqrCqr [sub. p/Nq, q/p, r/ CCpqq in L19]

2. CCCNqpCCpqqCpCCpqq

3. CCNpqCCqpp [sub. p/q, q/p in L15]

4. CCNqpCCpqq

5. CpCCpqq [(2)/(4) MP] Q.E.D.

Axiomatic Proof of Modus Ponens using standard notation

Axiom 1: (P–>Q)–>((Q–>R)–>(P–>R))

Axiom 2: ~P–>(P–>P)

Axiom 3: P–>(~P–>Q)

Lemma 4: ((((Q–>R)–>(P–>R))–>S)–>((P–>Q)–>S))

- (P–>Q)–>((Q–>R)–>(P–>R)) [sub. P/(P–>Q), Q/((Q–>R)–>(P–>R)), R/S in Axiom 1]
- ((P–>Q)–>((Q–>R)–>(P–>R)))–>((((Q–>R)–>(P–>R))–>S)–>((P–>Q)–>S))
- ((((Q–>R)–>(P–>R))–>S)–>((P–>Q)–>S)) [(1)/(2) MP] Q.E.D.

Lemma 5: ((P–>(Q–>R))–>((S–>Q)–>(P–>(S–>R))))

- ((((Q–>R)–>(P–>R))–>S)–>((P–>Q)–>S)) [sub. Q/ (Q–>R), R/(S–>R), S/((S–>Q)–>(P–>(S–>R))) L4]
- (((((Q–>R)–>(S–>R))–>(P–>(S–>R)))–>((S–>Q)–>(P–>(S–>R))))–>((P–>(Q–>R))–>((S–>Q)–>(P–>(S–>R)))))
- ((((Q–>R)–>(P–>R))–>S)–>((P–>Q)–>S)) [sub. P/S, S/ (P–>(S–>R)) in L4]
- ((((Q–>R)–>(S–>R))–>(P–>(S–>R)))–>((S–>Q)–>(P–>(S–>R))))
- ((P–>(Q–>R))–>((S–>Q)–>(P–>(S–>R)))) [(2)/(4) MP] Q.E.D.

Lemma 6: ((P–>Q)–>(((P–>R)–>S)–>((Q–>R)–>S)))

- ((((Q–>R)–>(P–>R))–>S)–>((P–>Q)–>S)) [sub. s/ (((P–>R)–>S)–>((Q–>R)–>S)) in L4]
- ((((Q–>R)–>(P–>R))–>(((P–>R)–>S)–>((Q–>R)–>S)))–>((P–>Q)–>(((P–>R)–>S)–>((Q–>R)–>S))))
- (P–>Q)–>((Q–>R)–>(P–>R)) [sub. P/ (Q–>R), Q/ (P–>R), R/S in Axiom 1]
- ((Q–>R)–>(P–>R))–>(((P–>R)–>S)–>((Q–>R)–>S))
- ((P–>Q)–>(((P–>R)–>S)–>((Q–>R)–>S))) [(2)/(4) MP] Q.E.D.

Lemma 7: (T–>((P–>R)–>S))–>((P–>Q)–>(T–>((Q–>R)–>S)))

- ((P–>(Q–>R))–>((S–>Q)–>(P–>(S–>R)))) [sub. P/ (P–>Q), Q/ ((P–>R)–>S), R/ ((Q–>R)–>S), S/T in L5]
- (((P–>Q)–>(((P–>R)–>S)–>((Q–>R)–>S)))–>((T–>((P–>R)–>S))–>((P–>Q)–>(T–>((Q–>R)–>S)))))
- (T–>((P–>R)–>S))–>((P–>Q)–>(T–>((Q–>R)–>S))) [(2)/(L6) MP] Q.E.D.

Lemma 9: (((~P–>Q)–>R)–>(P–>R))

- (P–>Q)–>((Q–>R)–>(P–>R)) [sub. Q/(~P–>Q) in Axiom 1]
- (P–>(~P–>Q))–>(((~P–>Q)–>R)–>(P–>R))
- (((~P–>Q)–>R)–>(P–>R)) [(2)/Axiom 3 MP] Q.E.D.

Lemma 10: (P–>(((~P–>P)–>P)–>((Q–>P)–>P)))

- (((~P–>Q)–>R)–>(P–>R)) [sub. R/ (((~P–>P)–>P)–>((Q–>P)–>P)) in L9]
- (((~P–>Q)–>(((~P–>P)–>P)–>((Q–>P)–>P)))–>(P–>(((~P–>P)–>P)–>((Q–>P)–>P))))
- ((P–>Q)–>(((P–>R)–>S)–>((Q–>R)–>S))) [sub. P/~P, R/P, S/P in L6]
- ((~P–>Q)–>(((~P–>P)–>P)–>((Q–>P)–>P)))
- (P–>(((~P–>P)–>P)–>((Q–>P)–>P))) [(2)/(4) MP] Q.E.D.

Lemma 11: ((Q–>((~P–>P)–>P))–>((~P–>P)–>P))

- (P–>(((~P–>P)–>P)–>((Q–>P)–>P)))) [sub. P/ ((~P–>P)–>P) in L10]
- (((~P–>P)–>P)–>(((~P–>((~P–>P)–>P))–>((~P–>P)–>P))–>((Q–>((~P–>P)–>P))–> ((~P–>P)–>P))))
- (((~P–>((~P–>P)–>P))–>((~P–>P)–>P))–>((Q–>((~P–>P)–>P))–> ((~P–>P)–>P)))) [(2)/(Axiom 2)MP]
- ((~P–>P)–>P) [sub. P/ ((~P–>P)–>P) in Axiom 2]
- (((~P–>((~P–>P)–>P))–>((~P–>P)–>P)))
- ((Q–>((~P–>P)–>P))–>((~P–>P)–>P)) [(2)/(4) MP] Q.E.D.

Lemma 12: (T–>((~P–>P)–>P))

- (((~P–>Q)–>R)–>(P–>R)) [sub. P/T, Q/ ((~P–>P)–>P), R/ ((~P–>P)–>P) in L9]
- (((~T–>((~P–>P)–>P))–>((~P–>P)–>P))–>(T–>((~P–>P)–>P)))
- ((Q–>((~P–>P)–>P))–>((~P–>P)–>P)) [sub. Q/~T in L11]
- ((~T–>((~P–>P)–>P))–>((~P–>P)–>P))
- (T–>((~P–>P)–>P)) [(2)/(4) MP] Q.E.D.

Lemma 13: (~P–>Q)–>(T–>((Q–>P)–>P))

- (T–>((P–>R)–>S))–>((P–>Q)–>(T–>((Q–>R)–>S))) [sub. P/~P, R/P, S/P in L7]
- (T–>((~P–>P)–>P))–>((~P–>Q)–>(T–>((Q–>P)–>P)))
- ((~P–>Q)–>(T–>((Q–>P)–>P))) [(2)/(L12) MP] Q.E.D.

Lemma 14: (((T–>((Q–>P)–>P))–>R)–>((~P–>Q)–>R))

- (P–>Q)–>((Q–>R)–>(P–>R)) [sub. P/(~P–>Q), Q/(T–>((Q–>P)–>P)) in Axiom 1]
- ((~P–>Q)–>(T–>((Q–>P)–>P)))–>(((T–>((Q–>P)–>P))–>R)–>((~P–>Q)–>R))
- (((T–>((Q–>P)–>P))–>R)–>((~P–>Q)–>R)) [(2)/(L13) MP] Q.E.D.

Lemma 15: ((~P–>Q)–>((Q–>P)–>P))

- (((T–>((Q–>P)–>P))–>R)–>((~P–>Q)–>R)) [sub. T/ ~((Q–>P)–>P), R/((Q–>P)–>P) in L14]
- (((~((Q–>P)–>P)–>((Q–>P)–>P))–>((Q–>P)–>P))–>((~P–>Q)–>((Q–>P)–>P)))
- ((~P–>P)–>P) [sub. P/((Q–>P)–>P) in Axiom 2]
- ((~((Q–>P)–>P)–>((Q–>P)–>P))–>((Q–>P)–>P))
- ((~P–>Q)–>((Q–>P)–>P)) [(2)/(4) MP] Q.E.D.

Lemma 17: (P–>((Q–>P)–>P))

- (((~P–>Q)–>R)–>(P–>R)) [sub. R/((Q–>P)–>P) in L9]
- (((~P–>Q)–> ((Q–>P)–>P))–>(P–>((Q–>P)–>P)))
- (P–>((Q–>P)–>P)) [(2)/(L15) MP] Q.E.D.

Lemma 18: (Q–>(P–>Q))

- ((P–>(Q–>R))–>((S–>Q)–>(P–>(S–>R)))) [P/Q, Q/ (~P–>Q), R/Q, S/P in L5]
- ((Q–>((~P–>Q)–>Q))–>((P–>(~P–>Q))–>(Q–>(P–>Q))))
- (P–>((Q–>P)–>P)) [sub. P/Q, Q/~P in L17]
- (Q–>((~P–>Q)–>Q))
- ((P–>(~P–>Q))–>(Q–>(P–>Q))) [(2)/(4) MP]
- (Q–>(P–>Q)) [(5)/(Axiom 3) MP] Q.E.D.

Lemma 19: ((P–>Q)–>R)–>(Q–>R)

- (P–>Q)–>((Q–>R)–>(P–>R)) [sub. P/Q, Q/(P–>Q) in Axiom 1]
- (Q–>(P–>Q))–>(((P–>Q)–>R)–>(Q–>R))
- (((P–>Q)–>R)–>(Q–>R)) [(2)/(L18) MP] Q.E.D.

Modus Ponens: (P–>((P–>Q)–>Q))

- ((P–>Q)–>R)–>(Q–>R) [sub. P/~Q, Q/P, R/((P–>Q)–>Q) in L19]
- ((~Q–>P)–> ((P–>Q)–>Q))–>(P–>((P–>Q)–>Q))
- ((~P–>Q)–>((Q–>P)–>P)) [sub. P/Q, Q/P in L15]
- ((~Q–>P)–>((P–>Q)–>Q))
- (P–>((P–>Q)–>Q)) [(2)/(4) MP] Q.E.D.