Description: Obsolete version of hbsbw as of 23-May-2024. (Contributed by NM, 12-Aug-1993) (Revised by Gino Giotto, 10-Jan-2024) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | hbsbwOLD.1 | |- ( ph -> A. z ph ) |
|
| Assertion | hbsbwOLD | |- ( [ y / x ] ph -> A. z [ y / x ] ph ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hbsbwOLD.1 | |- ( ph -> A. z ph ) |
|
| 2 | 1 | nf5i | |- F/ z ph |
| 3 | 2 | nfsbv | |- F/ z [ y / x ] ph |
| 4 | 3 | nf5ri | |- ( [ y / x ] ph -> A. z [ y / x ] ph ) |