Metamath Proof Explorer
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, 7Oct2016)


Ref 
Expression 

Hypotheses 
nfand.1 
⊢ ( 𝜑 → Ⅎ 𝑥 𝜓 ) 


nfand.2 
⊢ ( 𝜑 → Ⅎ 𝑥 𝜒 ) 

Assertion 
nfand 
⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝜓 ∧ 𝜒 ) ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

nfand.1 
⊢ ( 𝜑 → Ⅎ 𝑥 𝜓 ) 
2 

nfand.2 
⊢ ( 𝜑 → Ⅎ 𝑥 𝜒 ) 
3 

dfan 
⊢ ( ( 𝜓 ∧ 𝜒 ) ↔ ¬ ( 𝜓 → ¬ 𝜒 ) ) 
4 
2

nfnd 
⊢ ( 𝜑 → Ⅎ 𝑥 ¬ 𝜒 ) 
5 
1 4

nfimd 
⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝜓 → ¬ 𝜒 ) ) 
6 
5

nfnd 
⊢ ( 𝜑 → Ⅎ 𝑥 ¬ ( 𝜓 → ¬ 𝜒 ) ) 
7 
3 6

nfxfrd 
⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝜓 ∧ 𝜒 ) ) 