Theorem nfald 2327

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

Syntax hints:   → wi 4  ∀wal 1538  ∃wex 1779  Ⅎwnf 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-10 2142  ax-11 2158  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-or 848  df-ex 1780  df-nf 1784

This theorem is referenced by:  nfexd  2328  dvelimhw  2343  nfald2  2443  nfmodv  2552  nfeqd  2902  nfabdw  2913  nfraldw  3274  nfiotadw  6441  nfixpw  8843  axrepndlem1  10486  axrepndlem2  10487  axunnd  10490  axpowndlem2  10492  axpowndlem4  10494  axregndlem2  10497  axinfndlem1  10499  axinfnd  10500  axacndlem4  10504  axacndlem5  10505  axacnd  10506  axsepg2  35049  axsepg2ALT  35050  axnulg  35059  bj-dvelimdv  36829  wl-mo2df  37548  wl-eudf  37550  wl-mo2t  37553  nfintd  49662