This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nf3an

Description: If x is not free in ph , ps , and ch , then it is not free in ( ph /\ ps /\ ch ) . (Contributed by Mario Carneiro, 11-Aug-2016)

Ref Expression
Hypotheses nfan.1 ⊢ Ⅎ x φ
nfan.2 ⊢ Ⅎ x ψ
nfan.3 ⊢ Ⅎ x χ
Assertion nf3an ⊢ Ⅎ x φ ∧ ψ ∧ χ

Proof

Step Hyp Ref Expression
1 nfan.1 ⊢ Ⅎ x φ
2 nfan.2 ⊢ Ⅎ x ψ
3 nfan.3 ⊢ Ⅎ x χ
4 df-3an ⊢ φ ∧ ψ ∧ χ ↔ φ ∧ ψ ∧ χ
5 1 2 nfan ⊢ Ⅎ x φ ∧ ψ
6 5 3 nfan ⊢ Ⅎ x φ ∧ ψ ∧ χ
7 4 6 nfxfr ⊢ Ⅎ x φ ∧ ψ ∧ χ