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
|- ( ph -> F/ x ps )
nfand.2
|- ( ph -> F/ x ch )
Assertion nfand
|- ( ph -> F/ x ( ps /\ ch ) )

Proof

Step Hyp Ref Expression
1 nfand.1
 |-  ( ph -> F/ x ps )
2 nfand.2
 |-  ( ph -> F/ x ch )
3 df-an
 |-  ( ( ps /\ ch ) <-> -. ( ps -> -. ch ) )
4 2 nfnd
 |-  ( ph -> F/ x -. ch )
5 1 4 nfimd
 |-  ( ph -> F/ x ( ps -> -. ch ) )
6 5 nfnd
 |-  ( ph -> F/ x -. ( ps -> -. ch ) )
7 3 6 nfxfrd
 |-  ( ph -> F/ x ( ps /\ ch ) )