Theorem nf5ri 2207

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

Syntax hints:   → wi 4  ∀wal 1545  Ⅎwnf 1790

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-12 2189

This theorem depends on definitions:  df-bi 208  df-ex 1787  df-nf 1791

This theorem is referenced by:  19.3  2214  alimd  2224  alrimi  2225  eximd  2228  nexd  2233  albid  2234  exbid  2235  hbs1  2285  hba1  2304  hban  2311  hb3an  2312  nfal  2332  hbex  2334  nfsbv  2339  cbv3v  2343  cbv3  2405  equs45f  2467  nfs1  2496  sb6f  2505  hbsb  2532  hbab1  2726  nfsab  2729  nfsabg  2730  nfcrii  2896  ralrimi  3237  hbra1  3276  nfralw  3286  bnj1316  35002  bnj1379  35012  bnj1468  35028  bnj958  35122  bnj981  35132  bnj1014  35143  bnj1128  35172  bnj1204  35194  bnj1279  35200  bnj1398  35216  bnj1408  35218  bnj1444  35225  bnj1445  35226  bnj1446  35227  bnj1447  35228  bnj1448  35229  bnj1449  35230  bnj1463  35237  bnj1312  35240  bnj1518  35246  bnj1519  35247  bnj1520  35248  bnj1525  35251  bj-cbv2v  37151  bj-equs45fv  37164  mpobi123f  38529