Theorem nf5ri 2237

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

Syntax hints:   → wi 4  ∀wal 1565  Ⅎwnf 1810

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-12 2219

This theorem depends on definitions:  df-bi 210  df-ex 1807  df-nf 1811

This theorem is referenced by:  19.3  2244  alimd  2254  alrimi  2255  eximd  2258  nexd  2263  albid  2264  exbid  2265  hbs1  2315  hba1  2334  hban  2341  hb3an  2342  nfal  2362  hbex  2364  nfsbv  2369  cbv3v  2373  cbv3  2435  equs45f  2497  nfs1  2526  sb6f  2535  hbsb  2562  hbab1  2756  nfsab  2759  nfsabg  2760  nfcrii  2926  ralrimi  3269  hbra1  3308  nfralw  3318  bnj1316  35152  bnj1379  35162  bnj1468  35178  bnj958  35272  bnj981  35282  bnj1014  35293  bnj1128  35322  bnj1204  35344  bnj1279  35350  bnj1398  35366  bnj1408  35368  bnj1444  35375  bnj1445  35376  bnj1446  35377  bnj1447  35378  bnj1448  35379  bnj1449  35380  bnj1463  35387  bnj1312  35390  bnj1518  35396  bnj1519  35397  bnj1520  35398  bnj1525  35401  bj-cbv2v  37321  bj-equs45fv  37334  mpobi123f  38700