Theorem nf5ri 2195

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 2191	1 ⊢ (𝜑 → ∀𝑥𝜑)

Syntax hints:   → wi 4  ∀wal 1538  Ⅎ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 1910  ax-6 1967  ax-7 2007  ax-12 2177

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

This theorem is referenced by:  19.3  2202  alimd  2212  alrimi  2213  eximd  2216  nexd  2221  albid  2222  exbid  2223  hbs1  2274  hba1  2293  hban  2300  hb3an  2301  nfal  2323  hbex  2325  nfsbv  2330  cbv3v  2337  cbv3  2402  equs45f  2464  nfs1  2493  sb6f  2502  hbsb  2529  hbab1  2723  nfsab  2727  nfsabg  2728  nfcrii  2900  ralrimi  3257  hbra1  3301  nfralw  3311  bnj1316  34834  bnj1379  34844  bnj1468  34860  bnj958  34954  bnj981  34964  bnj1014  34975  bnj1128  35004  bnj1204  35026  bnj1279  35032  bnj1398  35048  bnj1408  35050  bnj1444  35057  bnj1445  35058  bnj1446  35059  bnj1447  35060  bnj1448  35061  bnj1449  35062  bnj1463  35069  bnj1312  35072  bnj1518  35078  bnj1519  35079  bnj1520  35080  bnj1525  35083  bj-cbv2v  36799  bj-equs45fv  36812  mpobi123f  38169