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 1788	. . . 4 ⊢ (𝜑 → (∃𝑥𝜓 → ∀𝑥𝜓))
5	2, 4	alimd 2210	. . 3 ⊢ (𝜑 → (∀𝑦∃𝑥𝜓 → ∀𝑦∀𝑥𝜓))
6		ax-11 2155	. . 3 ⊢ (∀𝑦∀𝑥𝜓 → ∀𝑥∀𝑦𝜓)
7	1, 5, 6	syl56 36	. 2 ⊢ (𝜑 → (∃𝑥∀𝑦𝜓 → ∀𝑥∀𝑦𝜓))
8	7	nfd 1787	1 ⊢ (𝜑 → Ⅎ𝑥∀𝑦𝜓)

Syntax hints:   → wi 4  ∀wal 1535  ∃wex 1776  Ⅎwnf 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-10 2139  ax-11 2155  ax-12 2175

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

This theorem is referenced by:  nfexd  2328  dvelimhw  2346  nfald2  2448  nfmodv  2557  nfeqd  2914  nfabdw  2925  nfraldw  3307  nfiotadw  6519  nfixpw  8955  axrepndlem1  10630  axrepndlem2  10631  axunnd  10634  axpowndlem2  10636  axpowndlem4  10638  axregndlem2  10641  axinfndlem1  10643  axinfnd  10644  axacndlem4  10648  axacndlem5  10649  axacnd  10650  axsepg2  35075  axsepg2ALT  35076  axnulg  35085  bj-dvelimdv  36834  wl-mo2df  37551  wl-eudf  37553  wl-mo2t  37556  nfintd  48904