Theorem festinoALT

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