Theorem nf5ri 2192

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

Syntax hints:   → wi 4  ∀wal 1534  Ⅎwnf 1779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-12 2174

This theorem depends on definitions:  df-bi 207  df-ex 1776  df-nf 1780

This theorem is referenced by:  19.3  2199  alimd  2209  alrimi  2210  eximd  2213  nexd  2218  albid  2219  exbid  2220  hbs1  2271  hba1  2291  hban  2298  hb3an  2299  nfal  2321  hbex  2323  nfsbv  2328  cbv3v  2335  cbv3  2399  equs45f  2461  nfs1  2490  sb6f  2499  hbsb  2526  hbab1  2720  nfsab  2724  nfsabg  2725  nfcrii  2897  ralrimi  3254  hbra1  3298  nfralw  3308  bnj1316  34812  bnj1379  34822  bnj1468  34838  bnj958  34932  bnj981  34942  bnj1014  34953  bnj1128  34982  bnj1204  35004  bnj1279  35010  bnj1398  35026  bnj1408  35028  bnj1444  35035  bnj1445  35036  bnj1446  35037  bnj1447  35038  bnj1448  35039  bnj1449  35040  bnj1463  35047  bnj1312  35050  bnj1518  35056  bnj1519  35057  bnj1520  35058  bnj1525  35061  bj-cbv2v  36780  bj-equs45fv  36793  mpobi123f  38148