Re: How to prove this theorem with intuitionistic natural deduction?

0: P -> (Q -> R) (Premisse)
1: P /\ Q        (Assumption)
2: P             (/\E,1)
3: Q -> R        (->E,0,2)
4: Q             (/\E,1)
5: R             (->E,3,4)
6: P /\ Q -> R   (Discharge,1)
Julio Di Egidio schrieb:

Dear logicians,
 How to prove the following theorem with natural deduction in intuitionistic propositional logic (namely, no classical inference rules)?
    `(P -> Q -> R) |- (P /\ Q -> R)`
 Thanks for any help.
 -Julio