Theorem barbariALT

Alternate proof of barbari, shorter but using more axioms. See comment of dariiALT. (Contributed by David A. Wheeler, 27-Aug-2016.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses
barbari.maj
\( \vdash \forall x \, (\varphi \rightarrow \psi) \)
barbari.min
\( \vdash \forall x \, (\chi \rightarrow \varphi) \)
barbari.e
\( \vdash \exists x \, \chi \)
Conclusion
\( \vdash \exists x \, (\chi \wedge \psi) \)
Proof
l0
barbari.e
\( \vdash \exists x \, \chi \)
l1
barbari.maj
\( \vdash \forall x \, (\varphi \rightarrow \psi) \)
barbari.min
\( \vdash \forall x \, (\chi \rightarrow \varphi) \)
barbara l1 _
\( \vdash \forall x \, (\chi \rightarrow \psi) \)
spi _
ancli _
\( \vdash \chi \rightarrow \chi \wedge \psi \)
eximii l0 _