![]() |
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 2312. (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 2316 | . . 3 ⊢ (∃𝑥∀𝑦𝜓 → ∀𝑦∃𝑥𝜓) | |
2 | nfald.1 | . . . 4 ⊢ Ⅎ𝑦𝜑 | |
3 | nfald.2 | . . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜓) | |
4 | 3 | nfrd 1786 | . . . 4 ⊢ (𝜑 → (∃𝑥𝜓 → ∀𝑥𝜓)) |
5 | 2, 4 | alimd 2201 | . . 3 ⊢ (𝜑 → (∀𝑦∃𝑥𝜓 → ∀𝑦∀𝑥𝜓)) |
6 | ax-11 2147 | . . 3 ⊢ (∀𝑦∀𝑥𝜓 → ∀𝑥∀𝑦𝜓) | |
7 | 1, 5, 6 | syl56 36 | . 2 ⊢ (𝜑 → (∃𝑥∀𝑦𝜓 → ∀𝑥∀𝑦𝜓)) |
8 | 7 | nfd 1785 | 1 ⊢ (𝜑 → Ⅎ𝑥∀𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1532 ∃wex 1774 Ⅎwnf 1778 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-10 2130 ax-11 2147 ax-12 2167 |
This theorem depends on definitions: df-bi 206 df-or 846 df-ex 1775 df-nf 1779 |
This theorem is referenced by: nfexd 2318 dvelimhw 2336 nfald2 2439 nfmodv 2548 nfeqd 2903 nfabdw 2916 nfraldw 3297 nfraldwOLD 3309 nfiotadw 6501 nfixpw 8937 axrepndlem1 10626 axrepndlem2 10627 axunnd 10630 axpowndlem2 10632 axpowndlem4 10634 axregndlem2 10637 axinfndlem1 10639 axinfnd 10640 axacndlem4 10644 axacndlem5 10645 axacnd 10646 bj-dvelimdv 36569 wl-mo2df 37278 wl-eudf 37280 wl-mo2t 37283 nfintd 48455 |
Copyright terms: Public domain | W3C validator |