This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nfnan

Description: If x is not free in ph and ps , then it is not free in ( ph -/\ ps ) . (Contributed by Scott Fenton, 2-Jan-2018)

Ref Expression
Hypotheses nfan.1 ⊢ Ⅎ x φ
nfan.2 ⊢ Ⅎ x ψ
Assertion nfnan ⊢ Ⅎ x φ ⊼ ψ

Proof

Step Hyp Ref Expression
1 nfan.1 ⊢ Ⅎ x φ
2 nfan.2 ⊢ Ⅎ x ψ
3 df-nan ⊢ φ ⊼ ψ ↔ ¬ φ ∧ ψ
4 1 2 nfan ⊢ Ⅎ x φ ∧ ψ
5 4 nfn ⊢ Ⅎ x ¬ φ ∧ ψ
6 3 5 nfxfr ⊢ Ⅎ x φ ⊼ ψ