Description: A version of spim with a distinct variable requirement instead of a bound-variable hypothesis. Usage of this theorem is discouraged because it depends on ax-13 . See spimfv and spimvw for versions requiring fewer axioms. (Contributed by NM, 31-Jul-1993) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | spimv.1 | |- ( x = y -> ( ph -> ps ) ) |
|
| Assertion | spimv | |- ( A. x ph -> ps ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | spimv.1 | |- ( x = y -> ( ph -> ps ) ) |
|
| 2 | nfv | |- F/ x ps |
|
| 3 | 2 1 | spim | |- ( A. x ph -> ps ) |