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

Syntax hints:   → wi 4  ∀wal 1558  Ⅎwnf 1803

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-12 2212

This theorem depends on definitions:  df-bi 209  df-ex 1800  df-nf 1804

This theorem is referenced 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  3260  hbra1  3299  nfralw  3309  bnj1316  35115  bnj1379  35125  bnj1468  35141  bnj958  35235  bnj981  35245  bnj1014  35256  bnj1128  35285  bnj1204  35307  bnj1279  35313  bnj1398  35329  bnj1408  35331  bnj1444  35338  bnj1445  35339  bnj1446  35340  bnj1447  35341  bnj1448  35342  bnj1449  35343  bnj1463  35350  bnj1312  35353  bnj1518  35359  bnj1519  35360  bnj1520  35361  bnj1525  35364  bj-cbv2v  37283  bj-equs45fv  37296  mpobi123f  38661