# Metamath Proof Explorer

## Theorem festinoALT

Description: 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.)

Ref Expression
Hypotheses festino.maj ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to ¬{\psi }\right)$
festino.min ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({\chi }\wedge {\psi }\right)$
Assertion festinoALT ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({\chi }\wedge ¬{\phi }\right)$

### Proof

Step Hyp Ref Expression
1 festino.maj ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to ¬{\psi }\right)$
2 festino.min ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({\chi }\wedge {\psi }\right)$
3 1 spi ${⊢}{\phi }\to ¬{\psi }$
4 3 con2i ${⊢}{\psi }\to ¬{\phi }$
5 4 anim2i ${⊢}\left({\chi }\wedge {\psi }\right)\to \left({\chi }\wedge ¬{\phi }\right)$
6 2 5 eximii ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({\chi }\wedge ¬{\phi }\right)$