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  2329  hbex  2331  nfsbv  2336  cbv3v  2340  cbv3  2402  equs45f  2464  nfs1  2493  sb6f  2502  hbsb  2529  hbab1  2724  nfsab  2727  nfsabg  2728  nfcrii  2894  ralrimi  3236  hbra1  3275  nfralw  3285  bnj1316  34996  bnj1379  35006  bnj1468  35022  bnj958  35116  bnj981  35126  bnj1014  35137  bnj1128  35166  bnj1204  35188  bnj1279  35194  bnj1398  35210  bnj1408  35212  bnj1444  35219  bnj1445  35220  bnj1446  35221  bnj1447  35222  bnj1448  35223  bnj1449  35224  bnj1463  35231  bnj1312  35234  bnj1518  35240  bnj1519  35241  bnj1520  35242  bnj1525  35245  bj-cbv2v  37046  bj-equs45fv  37059  mpobi123f  38413