Description: Version of spei with a disjoint variable condition, which does not require ax-13 (neither ax-7 nor ax-12 ). (Contributed by BJ, 31-May-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | speivw.1 | |
|
speivw.2 | |
||
Assertion | speivw | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | speivw.1 | |
|
2 | speivw.2 | |
|
3 | 1 | biimprd | |
4 | 3 2 | speiv | |