![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfan1 | Structured version Visualization version GIF version |
Description: A closed form of nfan 1897. (Contributed by Mario Carneiro, 3-Oct-2016.) df-nf 1781 changed. (Revised by Wolf Lammen, 18-Sep-2021.) (Proof shortened by Wolf Lammen, 7-Jul-2022.) |
Ref | Expression |
---|---|
nfim1.1 | ⊢ Ⅎ𝑥𝜑 |
nfim1.2 | ⊢ (𝜑 → Ⅎ𝑥𝜓) |
Ref | Expression |
---|---|
nfan1 | ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-an 396 | . 2 ⊢ ((𝜑 ∧ 𝜓) ↔ ¬ (𝜑 → ¬ 𝜓)) | |
2 | nfim1.1 | . . . 4 ⊢ Ⅎ𝑥𝜑 | |
3 | nfim1.2 | . . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜓) | |
4 | 3 | nfnd 1856 | . . . 4 ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜓) |
5 | 2, 4 | nfim1 2197 | . . 3 ⊢ Ⅎ𝑥(𝜑 → ¬ 𝜓) |
6 | 5 | nfn 1855 | . 2 ⊢ Ⅎ𝑥 ¬ (𝜑 → ¬ 𝜓) |
7 | 1, 6 | nfxfr 1850 | 1 ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 Ⅎwnf 1780 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-12 2175 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-ex 1777 df-nf 1781 |
This theorem is referenced by: sb4b 2478 ralcom2 3375 sbcralt 3881 sbcrext 3882 csbiebt 3938 riota5f 7416 axrepndlem1 10630 axrepndlem2 10631 axunnd 10634 axpowndlem2 10636 axpowndlem3 10637 axpowndlem4 10638 axregndlem2 10641 axinfndlem1 10643 axinfnd 10644 axacndlem4 10648 axacndlem5 10649 axacnd 10650 fproddivf 16020 nfan1c 35066 wl-sbcom2d-lem1 37540 wl-mo2df 37551 wl-eudf 37553 wl-mo3t 37557 wl-ax11-lem4 37569 wl-ax11-lem6 37571 |
Copyright terms: Public domain | W3C validator |