Description: Since the converse holds by a1i , this inference shows that we can represent a not-free hypothesis with either F/ x ph (inference form) or ( ph -> F/ x ph ) (deduction form). (Contributed by NM, 17-Aug-2018) (Proof shortened by Wolf Lammen, 10-Jul-2019) Reduce axiom dependencies. (Revised by SN and Sky Winter, 23-Oct-2026)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | nf5di.1 | |- ( ph -> F/ x ph ) |
|
| Assertion | nf5di | |- F/ x ph |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nf5di.1 | |- ( ph -> F/ x ph ) |
|
| 2 | hbe1 | |- ( E. x ph -> A. x E. x ph ) |
|
| 3 | 1 | nfrd | |- ( ph -> ( E. x ph -> A. x ph ) ) |
| 4 | 3 | com12 | |- ( E. x ph -> ( ph -> A. x ph ) ) |
| 5 | 2 4 | eximdh | |- ( E. x ph -> ( E. x ph -> E. x A. x ph ) ) |
| 6 | 5 | pm2.43i | |- ( E. x ph -> E. x A. x ph ) |
| 7 | hbe1a | |- ( E. x A. x ph -> A. x ph ) |
|
| 8 | 6 7 | syl | |- ( E. x ph -> A. x ph ) |
| 9 | 8 | nfi | |- F/ x ph |