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	$$⊢\phi \to Ⅎx\psi$$
	nfand.2	$$⊢\phi \to Ⅎx\chi$$
	nfand.3	$$⊢\phi \to Ⅎx\theta$$
Assertion	nf3and	$$⊢\phi \to Ⅎx\left(\psi \wedge \chi \wedge \theta \right)$$

Proof

Step	Hyp	Ref	Expression
1		nfand.1	$$⊢\phi \to Ⅎx\psi$$
2		nfand.2	$$⊢\phi \to Ⅎx\chi$$
3		nfand.3	$$⊢\phi \to Ⅎx\theta$$
4		df-3an	$$⊢\left(\psi \wedge \chi \wedge \theta \right)\leftrightarrow \left(\left(\psi \wedge \chi \right)\wedge \theta \right)$$
5	1 2	nfand	$$⊢\phi \to Ⅎx\left(\psi \wedge \chi \right)$$
6	5 3	nfand	$$⊢\phi \to Ⅎx\left(\left(\psi \wedge \chi \right)\wedge \theta \right)$$
7	4 6	nfxfrd	$$⊢\phi \to Ⅎx\left(\psi \wedge \chi \wedge \theta \right)$$