![]() |
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 2331. (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 2335 | . . 3 ⊢ (∃𝑥∀𝑦𝜓 → ∀𝑦∃𝑥𝜓) | |
2 | nfald.1 | . . . 4 ⊢ Ⅎ𝑦𝜑 | |
3 | nfald.2 | . . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜓) | |
4 | 3 | nfrd 1793 | . . . 4 ⊢ (𝜑 → (∃𝑥𝜓 → ∀𝑥𝜓)) |
5 | 2, 4 | alimd 2210 | . . 3 ⊢ (𝜑 → (∀𝑦∃𝑥𝜓 → ∀𝑦∀𝑥𝜓)) |
6 | ax-11 2158 | . . 3 ⊢ (∀𝑦∀𝑥𝜓 → ∀𝑥∀𝑦𝜓) | |
7 | 1, 5, 6 | syl56 36 | . 2 ⊢ (𝜑 → (∃𝑥∀𝑦𝜓 → ∀𝑥∀𝑦𝜓)) |
8 | 7 | nfd 1792 | 1 ⊢ (𝜑 → Ⅎ𝑥∀𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1536 ∃wex 1781 Ⅎwnf 1785 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-10 2142 ax-11 2158 ax-12 2175 |
This theorem depends on definitions: df-bi 210 df-or 845 df-ex 1782 df-nf 1786 |
This theorem is referenced by: nfexd 2337 dvelimhw 2355 nfald2 2456 nfmodv 2618 nfeqd 2965 nfraldw 3187 nfiotadw 6286 nfixpw 8463 axrepndlem1 10003 axrepndlem2 10004 axunnd 10007 axpowndlem2 10009 axpowndlem4 10011 axregndlem2 10014 axinfndlem1 10016 axinfnd 10017 axacndlem4 10021 axacndlem5 10022 axacnd 10023 bj-dvelimdv 34290 wl-mo2df 34971 wl-eudf 34973 wl-mo2t 34976 nfintd 45203 |
Copyright terms: Public domain | W3C validator |