Theorem nf5ri 2231

Description: Consequence of the definition of not-free. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 15-Mar-2023.)

Hypothesis

Ref	Expression
nf5ri.1	⊢ Ⅎ𝑥𝜑

Assertion

Ref	Expression
nf5ri	⊢ (𝜑 → ∀𝑥𝜑)

Proof of Theorem nf5ri

Step	Hyp	Ref	Expression
1		nf5ri.1	. . 3 ⊢ Ⅎ𝑥𝜑
2	1	nfri 1822	. 2 ⊢ (∃𝑥𝜑 → ∀𝑥𝜑)
3	2	19.23bi 2227	1 ⊢ (𝜑 → ∀𝑥𝜑)

This proof depends on syntax axioms:   → wi 4  ∀wal 1568  Ⅎ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-12 2213

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

This theorem is used by:  19.3  2238  alimd  2248  alrimi  2249  eximd  2252  nexd  2257  albid  2258  exbid  2259  hbs1  2307  hba1  2326  hban  2333  hb3an  2334  nfal  2353  hbex  2355  nfsbv  2360  cbv3v  2364  cbv3  2426  equs45f  2488  nfs1  2517  sb6f  2526  hbsb  2553  hbab1  2747  nfsab  2750  nfsabg  2751  nfcrii  2917  ralrimi  3260  hbra1  3299  nfralw  3309  bnj1316  35330  bnj1379  35340  bnj1468  35356  bnj958  35450  bnj981  35460  bnj1014  35471  bnj1128  35500  bnj1204  35522  bnj1279  35528  bnj1398  35544  bnj1408  35546  bnj1444  35553  bnj1445  35554  bnj1446  35555  bnj1447  35556  bnj1448  35557  bnj1449  35558  bnj1463  35565  bnj1312  35568  bnj1518  35574  bnj1519  35575  bnj1520  35576  bnj1525  35579  bj-cbv2v  37542  bj-equs45fv  37555  mpobi123f  38911