![]() |
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 1946. (Contributed by Mario Carneiro, 3-Oct-2016.) df-nf 1828 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 387 | . 2 ⊢ ((𝜑 ∧ 𝜓) ↔ ¬ (𝜑 → ¬ 𝜓)) | |
2 | nfim1.1 | . . . 4 ⊢ Ⅎ𝑥𝜑 | |
3 | nfim1.2 | . . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜓) | |
4 | 3 | nfnd 1903 | . . . 4 ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜓) |
5 | 2, 4 | nfim1 2181 | . . 3 ⊢ Ⅎ𝑥(𝜑 → ¬ 𝜓) |
6 | 5 | nfn 1902 | . 2 ⊢ Ⅎ𝑥 ¬ (𝜑 → ¬ 𝜓) |
7 | 1, 6 | nfxfr 1897 | 1 ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 386 Ⅎwnf 1827 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2054 ax-12 2162 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-ex 1824 df-nf 1828 |
This theorem is referenced by: ralcom2 3289 sbcralt 3727 sbcrext 3728 csbiebt 3770 riota5f 6908 axrepndlem1 9749 axrepndlem2 9750 axunnd 9753 axpowndlem2 9755 axpowndlem3 9756 axpowndlem4 9757 axregndlem2 9760 axinfndlem1 9762 axinfnd 9763 axacndlem4 9767 axacndlem5 9768 axacnd 9769 fproddivf 15120 wl-sbcom2d-lem1 33950 wl-mo2df 33960 wl-eudf 33962 wl-mo3t 33966 wl-ax11-lem4 33973 wl-ax11-lem6 33975 |
Copyright terms: Public domain | W3C validator |