|   | 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 1899. (Contributed by Mario Carneiro, 3-Oct-2016.) df-nf 1784 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 1858 | . . . 4 ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜓) | 
| 5 | 2, 4 | nfim1 2199 | . . 3 ⊢ Ⅎ𝑥(𝜑 → ¬ 𝜓) | 
| 6 | 5 | nfn 1857 | . 2 ⊢ Ⅎ𝑥 ¬ (𝜑 → ¬ 𝜓) | 
| 7 | 1, 6 | nfxfr 1853 | 1 ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 Ⅎwnf 1783 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-12 2177 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-ex 1780 df-nf 1784 | 
| This theorem is referenced by: sb4b 2480 ralcom2 3377 sbcralt 3872 sbcrext 3873 csbiebt 3928 riota5f 7416 axrepndlem1 10632 axrepndlem2 10633 axunnd 10636 axpowndlem2 10638 axpowndlem3 10639 axpowndlem4 10640 axregndlem2 10643 axinfndlem1 10645 axinfnd 10646 axacndlem4 10650 axacndlem5 10651 axacnd 10652 fproddivf 16023 nfan1c 35087 wl-sbcom2d-lem1 37560 wl-mo2df 37571 wl-eudf 37573 wl-mo3t 37577 wl-ax11-lem4 37589 wl-ax11-lem6 37591 | 
| Copyright terms: Public domain | W3C validator |