Metamath Proof Explorer


Theorem nf4

Description: Alternate definition of nonfreeness. This definition uses only primitive symbols ( -> , -. , A. ). (Contributed by BJ, 16-Sep-2021)

Ref Expression
Assertion nf4 x φ ¬ x φ x ¬ φ

Proof

Step Hyp Ref Expression
1 nf3 x φ x φ x ¬ φ
2 df-or x φ x ¬ φ ¬ x φ x ¬ φ
3 1 2 bitri x φ ¬ x φ x ¬ φ