Theorem nf5ri 2196

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 2192	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 2008  ax-12 2178

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

This theorem is referenced by:  19.3  2203  alimd  2213  alrimi  2214  eximd  2217  nexd  2222  albid  2223  exbid  2224  hbs1  2274  hba1  2293  hban  2300  hb3an  2301  nfal  2322  hbex  2324  nfsbv  2329  cbv3v  2333  cbv3  2396  equs45f  2458  nfs1  2487  sb6f  2496  hbsb  2523  hbab1  2717  nfsab  2720  nfsabg  2721  nfcrii  2887  ralrimi  3236  hbra1  3277  nfralw  3287  bnj1316  34817  bnj1379  34827  bnj1468  34843  bnj958  34937  bnj981  34947  bnj1014  34958  bnj1128  34987  bnj1204  35009  bnj1279  35015  bnj1398  35031  bnj1408  35033  bnj1444  35040  bnj1445  35041  bnj1446  35042  bnj1447  35043  bnj1448  35044  bnj1449  35045  bnj1463  35052  bnj1312  35055  bnj1518  35061  bnj1519  35062  bnj1520  35063  bnj1525  35066  bj-cbv2v  36793  bj-equs45fv  36806  mpobi123f  38163