Theorem nf3and

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

Hypotheses
nfand.1
\( \vdash \varphi \rightarrow \Finv x \, \psi \)
nfand.2
\( \vdash \varphi \rightarrow \Finv x \, \chi \)
nfand.3
\( \vdash \varphi \rightarrow \Finv x \, \theta \)
Conclusion
\( \vdash \varphi \rightarrow \Finv x \, (\psi \wedge \chi \wedge \theta) \)
Proof
l0
df-3an
\( \vdash \psi \wedge \chi \wedge \theta \leftrightarrow \psi \wedge \chi \wedge \theta \)
l1
nfand.1
nfand.2
l3
nfand l1 _
nfand.3
nfand l3 _
\( \vdash \varphi \rightarrow \Finv x \, (\psi \wedge \chi \wedge \theta) \)
nfxfrd l0 _