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	|- F/ x ph
	nf.2	|- F/ x ps
Assertion	nfor	|- F/ x ( ph \/ ps )

Proof

Step	Hyp	Ref	Expression
1		nf.1	|- F/ x ph
2		nf.2	|- F/ x ps
3		df-or	|- ( ( ph \/ ps ) <-> ( -. ph -> ps ) )
4	1	nfn	|- F/ x -. ph
5	4 2	nfim	|- F/ x ( -. ph -> ps )
6	3 5	nfxfr	|- F/ x ( ph \/ ps )