Theorem nf5ri 2186

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

Syntax hints:   → wi 4  ∀wal 1537  Ⅎwnf 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-12 2169

This theorem depends on definitions:  df-bi 206  df-ex 1780  df-nf 1784

This theorem is referenced by:  19.3  2193  alimd  2203  alrimi  2204  eximd  2207  nexd  2212  albid  2213  exbid  2214  hbs1  2264  hba1  2288  hban  2295  hb3an  2296  nfal  2315  hbex  2317  nfsbv  2322  hbsbwOLD  2324  cbv3v  2330  cbv3  2395  equs45f  2457  nfs1  2490  sb6f  2499  hbsb  2527  hbab1  2722  nfsab  2726  nfsabg  2727  nfcrii  2896  nfcriiOLD  2897  ralrimi  3236  hbra1  3280  nfralw  3290  bnj1316  32849  bnj1379  32859  bnj1468  32875  bnj958  32969  bnj981  32979  bnj1014  32990  bnj1128  33019  bnj1204  33041  bnj1279  33047  bnj1398  33063  bnj1408  33065  bnj1444  33072  bnj1445  33073  bnj1446  33074  bnj1447  33075  bnj1448  33076  bnj1449  33077  bnj1463  33084  bnj1312  33087  bnj1518  33093  bnj1519  33094  bnj1520  33095  bnj1525  33098  bj-cbv2v  35029  bj-equs45fv  35042  mpobi123f  36368