Theorem nfald 2331

Description: Deduction form of nfal 2326. (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 2330	. . 3 ⊢ (∃𝑥∀𝑦𝜓 → ∀𝑦∃𝑥𝜓)
2		nfald.1	. . . 4 ⊢ Ⅎ𝑦𝜑
3		nfald.2	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜓)
4	3	nfrd 1792	. . . 4 ⊢ (𝜑 → (∃𝑥𝜓 → ∀𝑥𝜓))
5	2, 4	alimd 2217	. . 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 2182

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

This theorem is referenced by:  nfexd  2332  dvelimhw  2347  nfald2  2447  nfmodv  2557  nfeqd  2907  nfabdw  2918  nfraldw  3279  nfiotadw  6449  nfixpw  8852  axrepndlem1  10501  axrepndlem2  10502  axunnd  10505  axpowndlem2  10507  axpowndlem4  10509  axregndlem2  10512  axinfndlem1  10514  axinfnd  10515  axacndlem4  10519  axacndlem5  10520  axacnd  10521  axsepg2  35187  axsepg2ALT  35188  axnulg  35213  bj-dvelimdv  36995  wl-mo2df  37714  wl-eudf  37716  wl-mo2t  37719  nfintd  49860