Theorem daraptiALT

Alternate proof of darapti, 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
darapti.maj
\( \vdash \forall x \, (\varphi \rightarrow \psi) \)
darapti.min
\( \vdash \forall x \, (\varphi \rightarrow \chi) \)
darapti.e
\( \vdash \exists x \, \varphi \)
Conclusion
\( \vdash \exists x \, (\chi \wedge \psi) \)
Proof
l0
darapti.e
\( \vdash \exists x \, \varphi \)
darapti.min
\( \vdash \forall x \, (\varphi \rightarrow \chi) \)
l2
spi _
darapti.maj
\( \vdash \forall x \, (\varphi \rightarrow \psi) \)
spi _
jca l2 _
\( \vdash \varphi \rightarrow \chi \wedge \psi \)
eximii l0 _