Hilbert-style proof of $\Gamma\vdash\psi$ and $\Gamma\vdash\chi$ implies $\Gamma\vdash\psi\wedge\chi$ I am given the following Hilbert-style system (for intuitionistic propositional logic):
Axiom schemes:


*

*$\phi\vee\phi\rightarrow\phi$

*$\phi\rightarrow\phi\wedge\phi$

*$\phi\rightarrow\phi\vee\psi$

*$\phi\wedge\psi\rightarrow\phi$

*$\phi\vee\psi\rightarrow\psi\vee\phi$

*$\phi\wedge\psi\rightarrow\psi\vee\phi$

*$\bot\rightarrow\phi$


Inference rules:


*$\phi$ and $\phi\rightarrow\psi$ imply $\psi$

*$\phi\rightarrow\psi$ and $\psi\rightarrow\chi$ imply $\phi\rightarrow \chi$

*$\phi\wedge\psi\rightarrow\chi$ implies $\phi\rightarrow(\psi\rightarrow\chi)$

*$\phi\rightarrow(\psi\rightarrow\chi)$ implies $\phi\wedge\psi\rightarrow\chi$

*$\phi\rightarrow\psi$ implies $\phi\vee\chi\rightarrow\psi\vee\chi$


We define, for a set $\Gamma$ of propositional formulas and a formula $\phi$, we define $\Gamma\vdash_{IL}\phi$ as ''There exists a proof in this Hilbert-style proof system (for intuitionistic logic) of $\phi$ from $\Gamma$.
I am now asked to prove (in essence, the actual question is broader): $$\text{if }\Gamma\vdash_{IL}\psi\text{ and }\Gamma\vdash_{IL}\chi\text{, then }\Gamma\vdash_{IL}\psi\wedge\chi$$
In a proof system like natural deduction, this would be proved by a conjunction introduction, but using above Hilbert-rules, I have not in any way been able to get some kind of conjunction introduction. For instance, using axiom scheme 2 didn't get me anywhere, we could think of substituting $(\psi\wedge\chi)$ for $\phi$, or just substituting $\psi$ for $\phi$, but no inference rule will then get us to the wanted conclusion.
Can the statement be proved using this Hilbert system?
 A: You can prove $$\psi\land \chi \to \psi\land\chi$$ by going through $(\psi\land\chi)\land(\psi\land\chi)$. Now apply rule 10 to get
$$ \psi \to (\chi\to\psi\land\chi) $$
Then your assumed derivations of $\psi$ and $\chi$, plus modus ponens twice concludes $\psi\land \chi$.
A: I use Polish notation.  The formation rules run:


*

*All lower case letters of the Latin alphabet, and 0 qualify as well-formed formulas (wffs).

*If $\alpha$ and $\beta$ qualify as wffs, then so do N$\alpha$, C$\alpha$$\beta$, K$\alpha$$\beta$, and A$\alpha$$\beta$.


The axiom schemes are:


*

*CAppp a law of Clavius

*CpKpp a law of K-tautology introduction

*CpApq left disjunction introduction

*CKpqp left conjunction elimination

*CApqAqp A-commutation

*CKpqApq conjunction comes as weaker than disjunction

*C0p falsum implies any proposition


The inference rules go:


*$\alpha$, C$\alpha$$\beta$ $\vdash$ $\beta$ modus ponens

*C$\alpha$$\beta$, C$\beta$$\gamma$ $\vdash$ C$\alpha$$\gamma$ hypothetical syllogism

*CK$\alpha$$\beta$$\gamma$ $\vdash$ C$\alpha$C$\beta$$\gamma$ exportation

*C$\alpha$C$\beta$$\gamma$ $\vdash$ CK$\alpha$$\beta$$\gamma$ importation

*C$\alpha$$\beta$ $\vdash$ CA$\alpha$$\gamma$A$\beta$$\gamma$
Now substituting q with p (q/p hereafter) in 3 we obtain


*CpApp


Applying hypothetical syllogism to 13 and 1 we thus obtain


*Cpp


Substituting p with Kpq in 14 we obtain


*CKpqKpq


Now applying exportation to 15 we obtain


*CpCqKpq


And I think you can do the rest.
