Description: No variable is (effectively) free in a theorem. (Contributed by Mario Carneiro, 11-Aug-2016) df-nf changed. (Revised by Wolf Lammen, 12-Sep-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | nfth.1 | |- ph |
|
| Assertion | nfth | |- F/ x ph |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfth.1 | |- ph |
|
| 2 | nftht | |- ( A. x ph -> F/ x ph ) |
|
| 3 | 2 1 | mpg | |- F/ x ph |