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}[3]{#3 \RightLabel{$\rightarrow$I,#1}\UnaryInfC{#2}}
\newcommand{\imple}[3]{#2 #3 \RightLabel{$\rightarrow$E}\BinaryInfC{#1}}

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

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

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

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

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

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

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

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

\end{document}