Theorem nf5ri 2232

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1568  Ⅎwnf 1816

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-12 2213

This proof depends on definitions:  df-bi 210  df-ex 1813  df-nf 1817

This theorem is used by:  19.3  2239  alimd  2249  alrimi  2250  eximd  2253  nexd  2258  albid  2259  exbid  2260  hbs1  2308  hba1  2327  hban  2334  hb3an  2335  nfal  2354  hbex  2356  nfsbv  2361  cbv3v  2365  cbv3  2427  equs45f  2489  nfs1  2518  sb6f  2527  hbsb  2554  hbab1  2748  nfsab  2751  nfsabg  2752  nfcrii  2918  ralrimi  3261  hbra1  3300  nfralw  3310  bnj1316  35450  bnj1379  35460  bnj1468  35476  bnj958  35570  bnj981  35580  bnj1014  35591  bnj1128  35620  bnj1204  35642  bnj1279  35648  bnj1398  35664  bnj1408  35666  bnj1444  35673  bnj1445  35674  bnj1446  35675  bnj1447  35676  bnj1448  35677  bnj1449  35678  bnj1463  35685  bnj1312  35688  bnj1518  35694  bnj1519  35695  bnj1520  35696  bnj1525  35699  bj-cbv2v  37710  bj-equs45fv  37723  mpobi123f  39094