Description: The setvar x is not free in A. x ph . This corresponds to the axiom (4) of modal logic. Example in Appendix in Megill p. 450 (p. 19 of the preprint). Also Lemma 22 of Monk2 p. 114. (Contributed by NM, 24-Jan-1993) (Proof shortened by Wolf Lammen, 12-Oct-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | hba1 | |- ( A. x ph -> A. x A. x ph ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfa1 | |- F/ x A. x ph |
|
| 2 | 1 | nf5ri | |- ( A. x ph -> A. x A. x ph ) |