Description: Closed form of 19.3 and version of 19.9t with a universal quantifier. (Contributed by NM, 9-Nov-2020) (Proof shortened by BJ, 9-Oct-2022)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | 19.3t | |- ( F/ x ph -> ( A. x ph <-> ph ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sp | |- ( A. x ph -> ph ) |
|
| 2 | nf5r | |- ( F/ x ph -> ( ph -> A. x ph ) ) |
|
| 3 | 1 2 | impbid2 | |- ( F/ x ph -> ( A. x ph <-> ph ) ) |