Theorem nf3and

Description: Deduction form of bound-variable hypothesis builder nf3an . (Contributed by NM, 17-Feb-2013) (Revised by Mario Carneiro, 16-Oct-2016)

	Ref	Expression
Hypotheses	nfand.1	|- ( ph -> F/ x ps )
	nfand.2	|- ( ph -> F/ x ch )
	nfand.3	|- ( ph -> F/ x th )
Assertion	nf3and	|- ( ph -> F/ x ( ps /\ ch /\ th ) )

Proof

Step	Hyp	Ref	Expression
1		nfand.1	|- ( ph -> F/ x ps )
2		nfand.2	|- ( ph -> F/ x ch )
3		nfand.3	|- ( ph -> F/ x th )
4		df-3an	|- ( ( ps /\ ch /\ th ) <-> ( ( ps /\ ch ) /\ th ) )
5	1 2	nfand	|- ( ph -> F/ x ( ps /\ ch ) )
6	5 3	nfand	|- ( ph -> F/ x ( ( ps /\ ch ) /\ th ) )
7	4 6	nfxfrd	|- ( ph -> F/ x ( ps /\ ch /\ th ) )