Theorem nf5ri 2230

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-12 2212

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

This theorem is used by:  19.3  2237  alimd  2247  alrimi  2248  eximd  2251  nexd  2256  albid  2257  exbid  2258  hbs1  2308  hba1  2327  hban  2334  hb3an  2335  nfal  2355  hbex  2357  nfsbv  2362  cbv3v  2366  cbv3  2428  equs45f  2490  nfs1  2519  sb6f  2528  hbsb  2555  hbab1  2749  nfsab  2752  nfsabg  2753  nfcrii  2919  ralrimi  3262  hbra1  3301  nfralw  3311  bnj1316  35217  bnj1379  35227  bnj1468  35243  bnj958  35337  bnj981  35347  bnj1014  35358  bnj1128  35387  bnj1204  35409  bnj1279  35415  bnj1398  35431  bnj1408  35433  bnj1444  35440  bnj1445  35441  bnj1446  35442  bnj1447  35443  bnj1448  35444  bnj1449  35445  bnj1463  35452  bnj1312  35455  bnj1518  35461  bnj1519  35462  bnj1520  35463  bnj1525  35466  bj-cbv2v  37461  bj-equs45fv  37474  mpobi123f  38839