Theorem nf3or

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

	Ref	Expression
Hypotheses	nf.1	|- F/ x ph
	nf.2	|- F/ x ps
	nf.3	|- F/ x ch
Assertion	nf3or	|- F/ x ( ph \/ ps \/ ch )

Proof

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