|   | 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 1898. (Contributed by Mario Carneiro, 3-Oct-2016.) df-nf 1783 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 1857 | . . . 4 ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜓) | 
| 5 | 2, 4 | nfim1 2198 | . . 3 ⊢ Ⅎ𝑥(𝜑 → ¬ 𝜓) | 
| 6 | 5 | nfn 1856 | . 2 ⊢ Ⅎ𝑥 ¬ (𝜑 → ¬ 𝜓) | 
| 7 | 1, 6 | nfxfr 1852 | 1 ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 Ⅎwnf 1782 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-12 2176 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-ex 1779 df-nf 1783 | 
| This theorem is referenced by: sb4b 2479 ralcom2 3376 sbcralt 3871 sbcrext 3872 csbiebt 3927 riota5f 7417 axrepndlem1 10633 axrepndlem2 10634 axunnd 10637 axpowndlem2 10639 axpowndlem3 10640 axpowndlem4 10641 axregndlem2 10644 axinfndlem1 10646 axinfnd 10647 axacndlem4 10651 axacndlem5 10652 axacnd 10653 fproddivf 16024 nfan1c 35088 wl-sbcom2d-lem1 37561 wl-mo2df 37572 wl-eudf 37574 wl-mo3t 37578 wl-ax11-lem4 37590 wl-ax11-lem6 37592 | 
| Copyright terms: Public domain | W3C validator |