Theorem nfald 2333

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

Syntax hints:   → wi 4  ∀wal 1539  ∃wex 1780  Ⅎwnf 1784

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-10 2146  ax-11 2162  ax-12 2184

This theorem depends on definitions:  df-bi 207  df-or 848  df-ex 1781  df-nf 1785

This theorem is referenced by:  nfexd  2334  dvelimhw  2349  nfald2  2449  nfmodv  2559  nfeqd  2909  nfabdw  2920  nfraldw  3281  nfiotadw  6451  nfixpw  8854  axrepndlem1  10503  axrepndlem2  10504  axunnd  10507  axpowndlem2  10509  axpowndlem4  10511  axregndlem2  10514  axinfndlem1  10516  axinfnd  10517  axacndlem4  10521  axacndlem5  10522  axacnd  10523  axsepg2  35238  axsepg2ALT  35239  axnulg  35264  mh-setindnd  36667  bj-dvelimdv  37052  wl-mo2df  37775  wl-eudf  37777  wl-mo2t  37780  nfintd  49918