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 2139. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 6-Jan-2018.) (Proof shortened by Wolf Lammen, 16-Oct-2021.) |
Ref | Expression |
---|---|
nfald.1 | ⊢ Ⅎ𝑦𝜑 |
nfald.2 | ⊢ (𝜑 → Ⅎ𝑥𝜓) |
Ref | Expression |
---|---|
nfald | ⊢ (𝜑 → Ⅎ𝑥∀𝑦𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 19.12 2150 | . . 3 ⊢ (∃𝑥∀𝑦𝜓 → ∀𝑦∃𝑥𝜓) | |
2 | nfald.1 | . . . 4 ⊢ Ⅎ𝑦𝜑 | |
3 | nfald.2 | . . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜓) | |
4 | 3 | nfrd 1708 | . . . 4 ⊢ (𝜑 → (∃𝑥𝜓 → ∀𝑥𝜓)) |
5 | 2, 4 | alimd 2068 | . . 3 ⊢ (𝜑 → (∀𝑦∃𝑥𝜓 → ∀𝑦∀𝑥𝜓)) |
6 | ax-11 2021 | . . 3 ⊢ (∀𝑦∀𝑥𝜓 → ∀𝑥∀𝑦𝜓) | |
7 | 1, 5, 6 | syl56 35 | . 2 ⊢ (𝜑 → (∃𝑥∀𝑦𝜓 → ∀𝑥∀𝑦𝜓)) |
8 | 7 | nfd 1707 | 1 ⊢ (𝜑 → Ⅎ𝑥∀𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1473 ∃wex 1695 Ⅎwnf 1699 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 |
This theorem depends on definitions: df-bi 196 df-or 384 df-ex 1696 df-nf 1701 |
This theorem is referenced by: nfexd 2153 dvelimhw 2159 nfald2 2319 nfeqd 2758 axrepndlem1 9293 axrepndlem2 9294 axunnd 9297 axpowndlem2 9299 axpowndlem4 9301 axregndlem2 9304 axinfndlem1 9306 axinfnd 9307 axacndlem4 9311 axacndlem5 9312 axacnd 9313 bj-dvelimdv 32027 wl-mo2df 32531 wl-eudf 32533 wl-mo2t 32536 nfintd 42218 |
Copyright terms: Public domain | W3C validator |