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 | |- A. x ( ph -> -. ps ) |
|
festino.min | |- E. x ( ch /\ ps ) |
||
Assertion | festinoALT | |- E. x ( ch /\ -. ph ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | festino.maj | |- A. x ( ph -> -. ps ) |
|
2 | festino.min | |- E. x ( ch /\ ps ) |
|
3 | 1 | spi | |- ( ph -> -. ps ) |
4 | 3 | con2i | |- ( ps -> -. ph ) |
5 | 4 | anim2i | |- ( ( ch /\ ps ) -> ( ch /\ -. ph ) ) |
6 | 2 5 | eximii | |- E. x ( ch /\ -. ph ) |