Theorem barocoALT

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