Description: A closed form of nfan . (Contributed by Mario Carneiro, 3-Oct-2016) df-nf changed. (Revised by Wolf Lammen, 18-Sep-2021) (Proof shortened by Wolf Lammen, 7-Jul-2022)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | nfim1.1 | |- F/ x ph |
|
| nfim1.2 | |- ( ph -> F/ x ps ) |
||
| Assertion | nfan1 | |- F/ x ( ph /\ ps ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfim1.1 | |- F/ x ph |
|
| 2 | nfim1.2 | |- ( ph -> F/ x ps ) |
|
| 3 | df-an | |- ( ( ph /\ ps ) <-> -. ( ph -> -. ps ) ) |
|
| 4 | 2 | nfnd | |- ( ph -> F/ x -. ps ) |
| 5 | 1 4 | nfim1 | |- F/ x ( ph -> -. ps ) |
| 6 | 5 | nfn | |- F/ x -. ( ph -> -. ps ) |
| 7 | 3 6 | nfxfr | |- F/ x ( ph /\ ps ) |