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	⊢ ( 𝜑 → Ⅎ 𝑥 𝜓 )
	nfand.2	⊢ ( 𝜑 → Ⅎ 𝑥 𝜒 )
	nfand.3	⊢ ( 𝜑 → Ⅎ 𝑥 𝜃 )
Assertion	nf3and	⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝜓 ∧ 𝜒 ∧ 𝜃 ) )

Proof

Step	Hyp	Ref	Expression
1		nfand.1	⊢ ( 𝜑 → Ⅎ 𝑥 𝜓 )
2		nfand.2	⊢ ( 𝜑 → Ⅎ 𝑥 𝜒 )
3		nfand.3	⊢ ( 𝜑 → Ⅎ 𝑥 𝜃 )
4		df-3an	⊢ ( ( 𝜓 ∧ 𝜒 ∧ 𝜃 ) ↔ ( ( 𝜓 ∧ 𝜒 ) ∧ 𝜃 ) )
5	1 2	nfand	⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝜓 ∧ 𝜒 ) )
6	5 3	nfand	⊢ ( 𝜑 → Ⅎ 𝑥 ( ( 𝜓 ∧ 𝜒 ) ∧ 𝜃 ) )
7	4 6	nfxfrd	⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝜓 ∧ 𝜒 ∧ 𝜃 ) )