Theorem nfbrd

Description: Deduction version of bound-variable hypothesis builder nfbr . (Contributed by NM, 13-Dec-2005) (Revised by Mario Carneiro, 14-Oct-2016)

	Ref	Expression
Hypotheses	nfbrd.2	|- ( ph -> F/_ x A )
	nfbrd.3	|- ( ph -> F/_ x R )
	nfbrd.4	|- ( ph -> F/_ x B )
Assertion	nfbrd	|- ( ph -> F/ x A R B )

Proof

Step	Hyp	Ref	Expression
1		nfbrd.2	|- ( ph -> F/_ x A )
2		nfbrd.3	|- ( ph -> F/_ x R )
3		nfbrd.4	|- ( ph -> F/_ x B )
4		df-br	|- ( A R B <-> <. A , B >. e. R )
5	1 3	nfopd	|- ( ph -> F/_ x <. A , B >. )
6	5 2	nfeld	|- ( ph -> F/ x <. A , B >. e. R )
7	4 6	nfxfrd	|- ( ph -> F/ x A R B )