Theorem nfald 2363

Description: Deduction form of nfal 2358. (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 2362	. . 3 ⊢ (∃𝑥∀𝑦𝜓 → ∀𝑦∃𝑥𝜓)
2		nfald.1	. . . 4 ⊢ Ⅎ𝑦𝜑
3		nfald.2	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜓)
4	3	nfrd 1824	. . . 4 ⊢ (𝜑 → (∃𝑥𝜓 → ∀𝑥𝜓))
5	2, 4	alimd 2251	. . 3 ⊢ (𝜑 → (∀𝑦∃𝑥𝜓 → ∀𝑦∀𝑥𝜓))
6		ax-11 2195	. . 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 1943  ax-6 2000  ax-7 2041  ax-10 2179  ax-11 2195  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  2364  dvelimhw  2379  nfald2  2479  nfmodv  2589  nfeqd  2937  nfabdw  2948  nfraldw  3312  nfiotadw  6499  nfixpw  8920  axrepndlem1  10594  axrepndlem2  10595  axunnd  10598  axpowndlem2  10600  axpowndlem4  10602  axregndlem2  10605  axinfndlem1  10607  axinfnd  10608  axacndlem4  10612  axacndlem5  10613  axacnd  10614  axsepg2  35612  axsepg3  35613  axsepg3ALT  35614  axsepg5  35616  axnulg  35617  axpowg2  35619  axpowg3  35620  mh-setindnd  37107  bj-dvelimdv  37545  wl-mo2df  38284  wl-eudf  38286  wl-mo2t  38289  nfintd  50510