Path: ...!weretis.net!feeder9.news.weretis.net!news.quux.org!eternal-september.org!feeder2.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: Julio Di Egidio <julio@diegidio.name>
Newsgroups: sci.logic
Subject: Re: How to prove this theorem with intuitionistic natural deduction?
Date: Mon, 18 Nov 2024 23:45:22 +0100
Organization: A noiseless patient Spider
Lines: 15
Message-ID: <vhgg23$19evr$2@dont-email.me>
References: <vhgdq0$19evr$1@dont-email.me> <vhgemi$ca9e$1@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Mon, 18 Nov 2024 23:45:23 +0100 (CET)
Injection-Info: dont-email.me; posting-host="3b9a6165cca410f94fcf9589e82bf7c4";
	logging-data="1358843"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX19t+sT+sSNH14dFnH1Rg4H2WSpQ6k1/JEQ="
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:0lqvaMmDv5/YjY2p1xJNaJa3Z8M=
In-Reply-To: <vhgemi$ca9e$1@solani.org>
Content-Language: en-GB
Bytes: 1499

On 18/11/2024 23:22, Mild Shock wrote:
> Julio Di Egidio schrieb:
>> `(P -> Q -> R) |- (P /\ Q -> R)`
> 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)

Wonderful, thank you.

-Julio