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 ) |