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