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 1821	. 2 ⊢ (∃𝑥𝜑 → ∀𝑥𝜑)
3	2	19.23bi 2227	1 ⊢ (𝜑 → ∀𝑥𝜑)

This proof depends on syntax axioms:   → wi 4  ∀wal 1567  Ⅎwnf 1815

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-12 2212

This proof depends on definitions:  df-bi 210  df-ex 1812  df-nf 1816

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  35500  bnj1379  35510  bnj1468  35526  bnj958  35620  bnj981  35630  bnj1014  35641  bnj1128  35670  bnj1204  35692  bnj1279  35698  bnj1398  35714  bnj1408  35716  bnj1444  35723  bnj1445  35724  bnj1446  35725  bnj1447  35726  bnj1448  35727  bnj1449  35728  bnj1463  35735  bnj1312  35738  bnj1518  35744  bnj1519  35745  bnj1520  35746  bnj1525  35749  bj-cbv2v  37834  bj-equs45fv  37847  mpobi123f  39231