Metamath Proof Explorer


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 φ x ψ
nfand.2 φ x χ
nfand.3 φ x θ
Assertion nf3and φ x ψ χ θ

Proof

Step Hyp Ref Expression
1 nfand.1 φ x ψ
2 nfand.2 φ x χ
3 nfand.3 φ x θ
4 df-3an ψ χ θ ψ χ θ
5 1 2 nfand φ x ψ χ
6 5 3 nfand φ x ψ χ θ
7 4 6 nfxfrd φ x ψ χ θ