Metamath Proof Explorer


Theorem nfor

Description: If x is not free in ph and ps , then it is not free in ( ph \/ ps ) . (Contributed by NM, 5-Aug-1993) (Revised by Mario Carneiro, 11-Aug-2016)

Ref Expression
Hypotheses nf.1 x φ
nf.2 x ψ
Assertion nfor x φ ψ

Proof

Step Hyp Ref Expression
1 nf.1 x φ
2 nf.2 x ψ
3 df-or φ ψ ¬ φ ψ
4 1 nfn x ¬ φ
5 4 2 nfim x ¬ φ ψ
6 3 5 nfxfr x φ ψ