![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfald | Structured version Visualization version GIF version |
Description: Deduction form of nfal 2357. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 16-Oct-2021.) |
Ref | Expression |
---|---|
nfald.1 | ⊢ Ⅎ𝑦𝜑 |
nfald.2 | ⊢ (𝜑 → Ⅎ𝑥𝜓) |
Ref | Expression |
---|---|
nfald | ⊢ (𝜑 → Ⅎ𝑥∀𝑦𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 19.12 2361 | . . 3 ⊢ (∃𝑥∀𝑦𝜓 → ∀𝑦∃𝑥𝜓) | |
2 | nfald.1 | . . . 4 ⊢ Ⅎ𝑦𝜑 | |
3 | nfald.2 | . . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜓) | |
4 | 3 | nfrd 1892 | . . . 4 ⊢ (𝜑 → (∃𝑥𝜓 → ∀𝑥𝜓)) |
5 | 2, 4 | alimd 2257 | . . 3 ⊢ (𝜑 → (∀𝑦∃𝑥𝜓 → ∀𝑦∀𝑥𝜓)) |
6 | ax-11 2209 | . . 3 ⊢ (∀𝑦∀𝑥𝜓 → ∀𝑥∀𝑦𝜓) | |
7 | 1, 5, 6 | syl56 36 | . 2 ⊢ (𝜑 → (∃𝑥∀𝑦𝜓 → ∀𝑥∀𝑦𝜓)) |
8 | 7 | nfd 1891 | 1 ⊢ (𝜑 → Ⅎ𝑥∀𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1656 ∃wex 1880 Ⅎwnf 1884 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-10 2194 ax-11 2209 ax-12 2222 |
This theorem depends on definitions: df-bi 199 df-or 881 df-ex 1881 df-nf 1885 |
This theorem is referenced by: nfexd 2363 dvelimhw 2371 nfald2 2466 nfmodv 2628 nfeqd 2977 axrepndlem1 9729 axrepndlem2 9730 axunnd 9733 axpowndlem2 9735 axpowndlem4 9737 axregndlem2 9740 axinfndlem1 9742 axinfnd 9743 axacndlem4 9747 axacndlem5 9748 axacnd 9749 bj-dvelimdv 33357 wl-mo2df 33896 wl-eudf 33898 wl-mo2t 33901 nfintd 43315 |
Copyright terms: Public domain | W3C validator |