Metamath Proof Explorer


Theorem hba1

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 x φ x x φ

Proof

Step Hyp Ref Expression
1 nfa1 x x φ
2 1 nf5ri x φ x x φ