Theorem nf5ri 2203

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

Syntax hints:   → wi 4  ∀wal 1540  Ⅎwnf 1785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-ex 1782  df-nf 1786

This theorem is referenced by:  19.3  2210  alimd  2220  alrimi  2221  eximd  2224  nexd  2229  albid  2230  exbid  2231  hbs1  2281  hba1  2300  hban  2307  hb3an  2308  nfal  2328  hbex  2330  nfsbv  2335  cbv3v  2339  cbv3  2401  equs45f  2463  nfs1  2492  sb6f  2501  hbsb  2528  hbab1  2723  nfsab  2726  nfsabg  2727  nfcrii  2893  ralrimi  3235  hbra1  3274  nfralw  3284  bnj1316  34962  bnj1379  34972  bnj1468  34988  bnj958  35082  bnj981  35092  bnj1014  35103  bnj1128  35132  bnj1204  35154  bnj1279  35160  bnj1398  35176  bnj1408  35178  bnj1444  35185  bnj1445  35186  bnj1446  35187  bnj1447  35188  bnj1448  35189  bnj1449  35190  bnj1463  35197  bnj1312  35200  bnj1518  35206  bnj1519  35207  bnj1520  35208  bnj1525  35211  bj-cbv2v  37105  bj-equs45fv  37118  mpobi123f  38483