![]() |
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 2317. (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 2321 | . . 3 ⊢ (∃𝑥∀𝑦𝜓 → ∀𝑦∃𝑥𝜓) | |
2 | nfald.1 | . . . 4 ⊢ Ⅎ𝑦𝜑 | |
3 | nfald.2 | . . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜓) | |
4 | 3 | nfrd 1794 | . . . 4 ⊢ (𝜑 → (∃𝑥𝜓 → ∀𝑥𝜓)) |
5 | 2, 4 | alimd 2206 | . . 3 ⊢ (𝜑 → (∀𝑦∃𝑥𝜓 → ∀𝑦∀𝑥𝜓)) |
6 | ax-11 2155 | . . 3 ⊢ (∀𝑦∀𝑥𝜓 → ∀𝑥∀𝑦𝜓) | |
7 | 1, 5, 6 | syl56 36 | . 2 ⊢ (𝜑 → (∃𝑥∀𝑦𝜓 → ∀𝑥∀𝑦𝜓)) |
8 | 7 | nfd 1793 | 1 ⊢ (𝜑 → Ⅎ𝑥∀𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1540 ∃wex 1782 Ⅎwnf 1786 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-10 2138 ax-11 2155 ax-12 2172 |
This theorem depends on definitions: df-bi 206 df-or 847 df-ex 1783 df-nf 1787 |
This theorem is referenced by: nfexd 2323 dvelimhw 2342 nfald2 2445 nfmodv 2554 nfeqd 2914 nfabdw 2927 nfraldw 3307 nfraldwOLD 3319 nfiotadw 6499 nfixpw 8910 axrepndlem1 10587 axrepndlem2 10588 axunnd 10591 axpowndlem2 10593 axpowndlem4 10595 axregndlem2 10598 axinfndlem1 10600 axinfnd 10601 axacndlem4 10605 axacndlem5 10606 axacnd 10607 bj-dvelimdv 35730 wl-mo2df 36435 wl-eudf 36437 wl-mo2t 36440 nfintd 47718 |
Copyright terms: Public domain | W3C validator |