Description: Alternate proof of darapti , 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 | darapti.maj | |- A. x ( ph -> ps ) |
|
darapti.min | |- A. x ( ph -> ch ) |
||
darapti.e | |- E. x ph |
||
Assertion | daraptiALT | |- E. x ( ch /\ ps ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | darapti.maj | |- A. x ( ph -> ps ) |
|
2 | darapti.min | |- A. x ( ph -> ch ) |
|
3 | darapti.e | |- E. x ph |
|
4 | 2 | spi | |- ( ph -> ch ) |
5 | 1 | spi | |- ( ph -> ps ) |
6 | 4 5 | jca | |- ( ph -> ( ch /\ ps ) ) |
7 | 3 6 | eximii | |- E. x ( ch /\ ps ) |