Theorem nf5ri 2200

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

Syntax hints:   → wi 4  ∀wal 1539  Ⅎwnf 1784

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-12 2182

This theorem depends on definitions:  df-bi 207  df-ex 1781  df-nf 1785

This theorem is referenced by:  19.3  2207  alimd  2217  alrimi  2218  eximd  2221  nexd  2226  albid  2227  exbid  2228  hbs1  2278  hba1  2297  hban  2304  hb3an  2305  nfal  2326  hbex  2328  nfsbv  2333  cbv3v  2337  cbv3  2399  equs45f  2461  nfs1  2490  sb6f  2499  hbsb  2526  hbab1  2721  nfsab  2724  nfsabg  2725  nfcrii  2891  ralrimi  3232  hbra1  3271  nfralw  3281  bnj1316  34925  bnj1379  34935  bnj1468  34951  bnj958  35045  bnj981  35055  bnj1014  35066  bnj1128  35095  bnj1204  35117  bnj1279  35123  bnj1398  35139  bnj1408  35141  bnj1444  35148  bnj1445  35149  bnj1446  35150  bnj1447  35151  bnj1448  35152  bnj1449  35153  bnj1463  35160  bnj1312  35163  bnj1518  35169  bnj1519  35170  bnj1520  35171  bnj1525  35174  bj-cbv2v  36942  bj-equs45fv  36955  mpobi123f  38302