Theorem nfald 2360

Description: Deduction form of nfal 2355. (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 2359	. . 3 ⊢ (∃𝑥∀𝑦𝜓 → ∀𝑦∃𝑥𝜓)
2		nfald.1	. . . 4 ⊢ Ⅎ𝑦𝜑
3		nfald.2	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜓)
4	3	nfrd 1811	. . . 4 ⊢ (𝜑 → (∃𝑥𝜓 → ∀𝑥𝜓))
5	2, 4	alimd 2247	. . 3 ⊢ (𝜑 → (∀𝑦∃𝑥𝜓 → ∀𝑦∀𝑥𝜓))
6		ax-11 2191	. . 3 ⊢ (∀𝑦∀𝑥𝜓 → ∀𝑥∀𝑦𝜓)
7	1, 5, 6	syl56 36	. 2 ⊢ (𝜑 → (∃𝑥∀𝑦𝜓 → ∀𝑥∀𝑦𝜓))
8	7	nfd 1810	1 ⊢ (𝜑 → Ⅎ𝑥∀𝑦𝜓)

Syntax hints:   → wi 4  ∀wal 1558  ∃wex 1799  Ⅎwnf 1803

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-10 2175  ax-11 2191  ax-12 2212

This theorem depends on definitions:  df-bi 209  df-or 859  df-ex 1800  df-nf 1804

This theorem is referenced by:  nfexd  2361  dvelimhw  2376  nfald2  2476  nfmodv  2586  nfeqd  2934  nfabdw  2945  nfraldw  3307  nfiotadw  6480  nfixpw  8898  axrepndlem1  10550  axrepndlem2  10551  axunnd  10554  axpowndlem2  10556  axpowndlem4  10558  axregndlem2  10561  axinfndlem1  10563  axinfnd  10564  axacndlem4  10568  axacndlem5  10569  axacnd  10570  axsepg2  35436  axsepg3  35437  axsepg3ALT  35438  axsepg5  35440  axnulg  35441  axpowg2  35443  axpowg3  35444  mh-setindnd  36897  bj-dvelimdv  37336  wl-mo2df  38073  wl-eudf  38075  wl-mo2t  38078  nfintd  50294