Natural deduction proof that $(P\leftrightarrow \neg P)$ is a contradiction, without first deriving $(P\vee \neg P)$ I'm looking to prove that $(P \leftrightarrow \neg P)$ is a contradiction using a natural deduction proof (which is to say, I want a proof to show $(P\leftrightarrow \neg P)\vdash Q$). In case it helps, the specific system I'm working in is as outlined in Halbach's Logic Manual (tree structure, introduction and elimination rules for each connective; see the link below), but it's the overall structure of the proof I'm struggling with.
Given a proof that shows $\vdash (P \vee \neg P)$ I can transform this into the desired proof, but that generates a very large tree given the simplicity of the sentence, because the proof for $\vdash (P \vee \neg P)$ is fairly long itself.
I can't shake the feeling there must be a more straightforward (even if still indirect) proof, but haven't been able to find it so far.

Edit: As found by lemontree, the ruleset I am using is listed here.
 A: One possible route is proving $\lnot(P \leftrightarrow \lnot P)$ without premises. Following that path, this would be a Gentzen-style proof, I think.
$
\def\be\qquad\mathbf{\leftrightarrow Elim}
\def\bi\qquad\mathbf{\leftrightarrow Intro}
\def\ne\qquad\mathbf{\neg Elim}
\def\ni\qquad\mathbf{\neg Intro}
$
$
\begin{equation}
  \dfrac{
    \dfrac{
      [P] \qquad [P \leftrightarrow \lnot P]
    }{
      \dfrac{
          [P] \qquad \lnot P
        }{\lnot P}\ni}\be
    \quad
    \dfrac{
      [\lnot P] \qquad [P \leftrightarrow \lnot P]
    }{
      \dfrac{
          [\lnot P] \qquad P
        }{P}\ne}\be
  }{\lnot(P \leftrightarrow \lnot P)}\ne
\end{equation}
$

EDIT:
Based on OP comments, I am adding a proof of $P \leftrightarrow \lnot P \vdash Q\\$.
$
\begin{equation}
  \dfrac{
    \dfrac{
      [P] \qquad P \leftrightarrow \lnot P
    }{
      \dfrac{
          [P] \qquad \lnot P
        }{\lnot P}\ni}\be
    \quad
    \dfrac{
      [\lnot P] \qquad P \leftrightarrow \lnot P
    }{
      \dfrac{
          [\lnot P] \qquad P
        }{P}\ne}\be
  }{Q}\ne
\end{equation}
$
A: You can prove Lemma 1: $P\to\lnot P\vdash\lnot P$:

*

*$P\to\lnot P$ - assumption

*| $P$ - additional assumption

*| $\lnot P$ - modus ponens on 1. and 2.

*| $\bot$ - elimination of negation from 2. and 3.

*$\lnot P$ - introduction of negation on 2-4.

and similarly Lemma 2: $\lnot P\to P\vdash P$. Now:

*

*$P\leftrightarrow\lnot P$ - assumption

*$P\to\lnot P$ - elimination of equivalence from 1.

*$\lnot P\to P$ - elimination of equivalence from 1.

*$P$ - Lemma 2 and 3.

*$\lnot P$ - Lemma 1 and 2.

*$\bot$ - elimination of negation from 5. and 6.

*$Q$ - ex falso quodlibet from 6.

A: (Posted after answer accepted.) Using a form of natural deduction:


