![]() |
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 1894. (Contributed by Mario Carneiro, 3-Oct-2016.) df-nf 1778 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 395 | . 2 ⊢ ((𝜑 ∧ 𝜓) ↔ ¬ (𝜑 → ¬ 𝜓)) | |
2 | nfim1.1 | . . . 4 ⊢ Ⅎ𝑥𝜑 | |
3 | nfim1.2 | . . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜓) | |
4 | 3 | nfnd 1853 | . . . 4 ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜓) |
5 | 2, 4 | nfim1 2187 | . . 3 ⊢ Ⅎ𝑥(𝜑 → ¬ 𝜓) |
6 | 5 | nfn 1852 | . 2 ⊢ Ⅎ𝑥 ¬ (𝜑 → ¬ 𝜓) |
7 | 1, 6 | nfxfr 1847 | 1 ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 394 Ⅎwnf 1777 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-12 2166 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-ex 1774 df-nf 1778 |
This theorem is referenced by: sb4b 2468 ralcom2 3360 sbcralt 3862 sbcrext 3863 csbiebt 3919 riota5f 7404 axrepndlem1 10617 axrepndlem2 10618 axunnd 10621 axpowndlem2 10623 axpowndlem3 10624 axpowndlem4 10625 axregndlem2 10628 axinfndlem1 10630 axinfnd 10631 axacndlem4 10635 axacndlem5 10636 axacnd 10637 fproddivf 15967 wl-sbcom2d-lem1 37157 wl-mo2df 37168 wl-eudf 37170 wl-mo3t 37174 wl-ax11-lem4 37186 wl-ax11-lem6 37188 |
Copyright terms: Public domain | W3C validator |