Theorem nfald 2350

Description: Deduction form of nfal 2345. (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 2349	. . 3 ⊢ (∃𝑥∀𝑦𝜓 → ∀𝑦∃𝑥𝜓)
2		nfald.1	. . . 4 ⊢ Ⅎ𝑦𝜑
3		nfald.2	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜓)
4	3	nfrd 1801	. . . 4 ⊢ (𝜑 → (∃𝑥𝜓 → ∀𝑥𝜓))
5	2, 4	alimd 2237	. . 3 ⊢ (𝜑 → (∀𝑦∃𝑥𝜓 → ∀𝑦∀𝑥𝜓))
6		ax-11 2181	. . 3 ⊢ (∀𝑦∀𝑥𝜓 → ∀𝑥∀𝑦𝜓)
7	1, 5, 6	syl56 36	. 2 ⊢ (𝜑 → (∃𝑥∀𝑦𝜓 → ∀𝑥∀𝑦𝜓))
8	7	nfd 1800	1 ⊢ (𝜑 → Ⅎ𝑥∀𝑦𝜓)

Syntax hints:   → wi 4  ∀wal 1548  ∃wex 1789  Ⅎwnf 1793

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-10 2165  ax-11 2181  ax-12 2202

This theorem depends on definitions:  df-bi 209  df-or 857  df-ex 1790  df-nf 1794

This theorem is referenced by:  nfexd  2351  dvelimhw  2366  nfald2  2466  nfmodv  2576  nfeqd  2924  nfabdw  2935  nfraldw  3297  nfiotadw  6465  nfixpw  8883  axrepndlem1  10536  axrepndlem2  10537  axunnd  10540  axpowndlem2  10542  axpowndlem4  10544  axregndlem2  10547  axinfndlem1  10549  axinfnd  10550  axacndlem4  10554  axacndlem5  10555  axacnd  10556  axsepg2  35381  axsepg3  35382  axsepg3ALT  35383  axsepg5  35385  axnulg  35386  axpowg2  35388  axpowg3  35389  mh-setindnd  36835  bj-dvelimdv  37274  wl-mo2df  38011  wl-eudf  38013  wl-mo2t  38016  nfintd  50232