Theorem nfald 2358

Description: Deduction form of nfal 2353. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 16-Oct-2021.)

Hypotheses

Ref	Expression
nfald.1	⊢ Ⅎ𝑦𝜑
nfald.2	⊢ (𝜑 → Ⅎ𝑥𝜓)

Assertion

Ref	Expression
nfald	⊢ (𝜑 → Ⅎ𝑥∀𝑦𝜓)

Proof of Theorem nfald

Step	Hyp	Ref	Expression
1		19.12 2357	. . 3 ⊢ (∃𝑥∀𝑦𝜓 → ∀𝑦∃𝑥𝜓)
2		nfald.1	. . . 4 ⊢ Ⅎ𝑦𝜑
3		nfald.2	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜓)
4	3	nfrd 1824	. . . 4 ⊢ (𝜑 → (∃𝑥𝜓 → ∀𝑥𝜓))
5	2, 4	alimd 2248	. . 3 ⊢ (𝜑 → (∀𝑦∃𝑥𝜓 → ∀𝑦∀𝑥𝜓))
6		ax-11 2194	. . 3 ⊢ (∀𝑦∀𝑥𝜓 → ∀𝑥∀𝑦𝜓)
7	1, 5, 6	syl56 37	. 2 ⊢ (𝜑 → (∃𝑥∀𝑦𝜓 → ∀𝑥∀𝑦𝜓))
8	7	nfd 1823	1 ⊢ (𝜑 → Ⅎ𝑥∀𝑦𝜓)

This proof depends on syntax axioms:   → wi 4  ∀wal 1568  ∃wex 1812  Ⅎwnf 1816

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-10 2178  ax-11 2194  ax-12 2213

This proof depends on definitions:  df-bi 210  df-or 862  df-ex 1813  df-nf 1817

This theorem is used by:  nfexd  2359  dvelimhw  2374  nfald2  2474  nfmodv  2584  nfeqd  2932  nfabdw  2943  nfraldw  3307  nfiotadw  6492  nfixpw  8924  axrepndlem1  10602  axrepndlem2  10603  axunnd  10606  axpowndlem2  10608  axpowndlem4  10610  axregndlem2  10613  axinfndlem1  10615  axinfnd  10616  axacndlem4  10620  axacndlem5  10621  axacnd  10622  axsepg2  35667  axsepg3  35668  axsepg3ALT  35669  axsepg5  35671  axnulg  35672  axpowg2  35674  axpowg3  35675  mh-setindnd  37157  bj-dvelimdv  37595  wl-mo2df  38334  wl-eudf  38336  wl-mo2t  38339  nfintd  50600