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

Metamath Proof Explorer

Theorem nfand

Description: If in a context x is not free in ps and ch , then it is not free in ( ps /\ ch ) . (Contributed by Mario Carneiro, 7-Oct-2016)

Ref Expression
Hypotheses nfand.1 ⊢ ( 𝜑 → Ⅎ 𝑥 𝜓 )
nfand.2 ⊢ ( 𝜑 → Ⅎ 𝑥 𝜒 )
Assertion nfand ( 𝜑 → Ⅎ 𝑥 ( 𝜓 ∧ 𝜒 ) )

Proof

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