| 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 2323. (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 2327 | . . 3 ⊢ (∃𝑥∀𝑦𝜓 → ∀𝑦∃𝑥𝜓) | |
| 2 | nfald.1 | . . . 4 ⊢ Ⅎ𝑦𝜑 | |
| 3 | nfald.2 | . . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜓) | |
| 4 | 3 | nfrd 1791 | . . . 4 ⊢ (𝜑 → (∃𝑥𝜓 → ∀𝑥𝜓)) |
| 5 | 2, 4 | alimd 2212 | . . 3 ⊢ (𝜑 → (∀𝑦∃𝑥𝜓 → ∀𝑦∀𝑥𝜓)) |
| 6 | ax-11 2157 | . . 3 ⊢ (∀𝑦∀𝑥𝜓 → ∀𝑥∀𝑦𝜓) | |
| 7 | 1, 5, 6 | syl56 36 | . 2 ⊢ (𝜑 → (∃𝑥∀𝑦𝜓 → ∀𝑥∀𝑦𝜓)) |
| 8 | 7 | nfd 1790 | 1 ⊢ (𝜑 → Ⅎ𝑥∀𝑦𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∀wal 1538 ∃wex 1779 Ⅎwnf 1783 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-10 2141 ax-11 2157 ax-12 2177 |
| This theorem depends on definitions: df-bi 207 df-or 849 df-ex 1780 df-nf 1784 |
| This theorem is referenced by: nfexd 2329 dvelimhw 2347 nfald2 2450 nfmodv 2559 nfeqd 2916 nfabdw 2927 nfraldw 3309 nfiotadw 6517 nfixpw 8956 axrepndlem1 10632 axrepndlem2 10633 axunnd 10636 axpowndlem2 10638 axpowndlem4 10640 axregndlem2 10643 axinfndlem1 10645 axinfnd 10646 axacndlem4 10650 axacndlem5 10651 axacnd 10652 axsepg2 35096 axsepg2ALT 35097 axnulg 35106 bj-dvelimdv 36852 wl-mo2df 37571 wl-eudf 37573 wl-mo2t 37576 nfintd 49192 |
| Copyright terms: Public domain | W3C validator |