Theorem nfald 2362

Description: Deduction form of nfal 2357. (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 2361	. . 3 ⊢ (∃𝑥∀𝑦𝜓 → ∀𝑦∃𝑥𝜓)
2		nfald.1	. . . 4 ⊢ Ⅎ𝑦𝜑
3		nfald.2	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜓)
4	3	nfrd 1824	. . . 4 ⊢ (𝜑 → (∃𝑥𝜓 → ∀𝑥𝜓))
5	2, 4	alimd 2252	. . 3 ⊢ (𝜑 → (∀𝑦∃𝑥𝜓 → ∀𝑦∀𝑥𝜓))
6		ax-11 2197	. . 3 ⊢ (∀𝑦∀𝑥𝜓 → ∀𝑥∀𝑦𝜓)
7	1, 5, 6	syl56 37	. 2 ⊢ (𝜑 → (∃𝑥∀𝑦𝜓 → ∀𝑥∀𝑦𝜓))
8	7	nfd 1823	1 ⊢ (𝜑 → Ⅎ𝑥∀𝑦𝜓)

This proof depends on syntax axioms:   → wi 4  ∀wal 1568  ∃wex 1812  Ⅎwnf 1816

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-10 2180  ax-11 2197  ax-12 2216

This proof depends on definitions:  df-bi 210  df-or 862  df-ex 1813  df-nf 1817

This theorem is used by:  nfexd  2363  dvelimhw  2378  nfald2  2477  nfmodv  2587  nfeqd  2936  nfabdw  2947  nfraldw  3311  nfiotadw  6523  nfixpw  8982  axrepndlem1  10716  axrepndlem2  10717  axunnd  10720  axpowndlem2  10722  axpowndlem4  10724  axregndlem2  10727  axinfndlem1  10729  axinfnd  10730  axacndlem4  10734  axacndlem5  10735  axacnd  10736  axsepg2  35949  axsepg3  35950  axsepg3ALT  35951  axsepg5  35953  axnulg  35954  axpowg2  35956  axpowg3  35957  mh-setindnd  37540  bj-dvelimdv  37978  wl-mo2df  38770  wl-eudf  38772  wl-mo2t  38775  nfintd  51187