Theorem nfald 2337

Description: Deduction form of nfal 2332. (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 2336	. . 3 ⊢ (∃𝑥∀𝑦𝜓 → ∀𝑦∃𝑥𝜓)
2		nfald.1	. . . 4 ⊢ Ⅎ𝑦𝜑
3		nfald.2	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜓)
4	3	nfrd 1798	. . . 4 ⊢ (𝜑 → (∃𝑥𝜓 → ∀𝑥𝜓))
5	2, 4	alimd 2224	. . 3 ⊢ (𝜑 → (∀𝑦∃𝑥𝜓 → ∀𝑦∀𝑥𝜓))
6		ax-11 2168	. . 3 ⊢ (∀𝑦∀𝑥𝜓 → ∀𝑥∀𝑦𝜓)
7	1, 5, 6	syl56 36	. 2 ⊢ (𝜑 → (∃𝑥∀𝑦𝜓 → ∀𝑥∀𝑦𝜓))
8	7	nfd 1797	1 ⊢ (𝜑 → Ⅎ𝑥∀𝑦𝜓)

Syntax hints:   → wi 4  ∀wal 1545  ∃wex 1786  Ⅎwnf 1790

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-10 2152  ax-11 2168  ax-12 2189

This theorem depends on definitions:  df-bi 208  df-or 854  df-ex 1787  df-nf 1791

This theorem is referenced by:  nfexd  2338  dvelimhw  2353  nfald2  2453  nfmodv  2563  nfeqd  2911  nfabdw  2922  nfraldw  3284  nfiotadw  6444  nfixpw  8854  axrepndlem1  10506  axrepndlem2  10507  axunnd  10510  axpowndlem2  10512  axpowndlem4  10514  axregndlem2  10517  axinfndlem1  10519  axinfnd  10520  axacndlem4  10524  axacndlem5  10525  axacnd  10526  axsepg2  35321  axsepg3  35322  axsepg3ALT  35323  axsepg5  35325  axnulg  35326  axpowg2  35328  axpowg3  35329  mh-setindnd  36765  bj-dvelimdv  37204  wl-mo2df  37941  wl-eudf  37943  wl-mo2t  37946  nfintd  50163