Metamath Proof Explorer

Theorem hbe1

Description: The setvar x is not free in E. x ph . Corresponds to the axiom (5) of modal logic (see also modal5 ). (Contributed by NM, 24-Jan-1993)

Ref Expression
Assertion hbe1 x φ x x φ


Step Hyp Ref Expression
1 df-ex x φ ¬ x ¬ φ
2 hbn1 ¬ x ¬ φ x ¬ x ¬ φ
3 1 2 hbxfrbi x φ x x φ