Description: Obsolete version of nfsb as of 25-Feb-2024. (Contributed by Mario Carneiro, 11-Aug-2016) (New usage is discouraged.) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | nfsb.1 | |- F/ z ph |
|
| Assertion | nfsbOLD | |- F/ z [ y / x ] ph |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfsb.1 | |- F/ z ph |
|
| 2 | axc16nf | |- ( A. z z = y -> F/ z [ y / x ] ph ) |
|
| 3 | 1 | nfsb4 | |- ( -. A. z z = y -> F/ z [ y / x ] ph ) |
| 4 | 2 3 | pm2.61i | |- F/ z [ y / x ] ph |