Natural deduction with handy latex commands

natded.tex

\documentclass[a4paper]{article}
\usepackage{bussproofs}
\usepackage{savetrees}
\usepackage{amsmath}

\newcommand{\using}[2]{\AxiomC{}\RightLabel{#1}\UnaryInfC{#2}}

\newcommand{\assume}[1]{\AxiomC{#1}}
\newcommand{\closed}[2]{\AxiomC{$\left[\text{#2}\right]^\text{#1}$}}

\newcommand{\impli}[2]{\RightLabel{$\rightarrow$I,#1}\UnaryInfC{#2}}
\newcommand{\imple}[1]{\RightLabel{$\rightarrow$E}\BinaryInfC{#1}}

\newcommand{\disji}[1]{\RightLabel{$\lor$I}\UnaryInfC{#1}}
\newcommand{\disje}[2]{\RightLabel{$\lor$E,#1}\TrinaryInfC{#2}}

\newcommand{\conji}[1]{\RightLabel{$\land$I}\BinaryInfC{#1}}
\newcommand{\conje}[2]{\RightLabel{$\land$E,#1}\BinaryInfC{#2}}

\newcommand{\univi}[1]{\RightLabel{$\forall$I}\UnaryInfC{#1}}
\newcommand{\unive}[1]{\RightLabel{$\forall$E}\UnaryInfC{#1}}

\newcommand{\exisi}[1]{\RightLabel{$\exists$I}\UnaryInfC{#1}}
\newcommand{\exise}[2]{\RightLabel{$\exists$E,#1}\BinaryInfC{#2}}

\begin{document}
\begin{prooftree}
	\closed{1}{$Px \rightarrow Qs$} \assume{$Px$}
	\imple{$Qs$}
	\impli{1}{$(Px \rightarrow Qs) \rightarrow Qs$}
\end{prooftree}

\begin{prooftree}
	\using{LEM}{$P \lor \lnot P$}
		\closed{1}{$P$}
		\disji{$P \lor Q$}
			\closed{1}{$\lnot P$}
			\UnaryInfC{$\vdots$}
			\UnaryInfC{$P \lor Q$}
			\disje{1}{$P \lor Q$}
\end{prooftree}

\begin{prooftree}
	\assume{$A$}
		\assume{$B$}
	\conji{$A \land B$}
		\assume{$A \rightarrow B \rightarrow C$}
			\closed{1}{$A$}
			\imple{$B \rightarrow C$}
				\closed{1}{$B$}
			\imple{$C$}
		\conje{1}{$C$}
\end{prooftree}

\begin{prooftree}
	\assume{$\exists x Px$}
		\using{Lemma}{$\forall x (Px \rightarrow Qx)$}
		\unive{$Px \rightarrow Qx$}
			\closed{1}{$Px$}
		\imple{$Qx$}
		\exisi{$\exists x Qx$}
	\exise{1}{$\exists x Qx$}
	\univi{$\forall y \exists x Qx$}
\end{prooftree}

\end{document}