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 ) ) |
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 ) ) |