Theorem nf5ri 2234

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 2230	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 2216

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

This theorem is used by:  19.3  2241  alimd  2251  alrimi  2252  eximd  2255  nexd  2260  albid  2261  exbid  2262  hbs1  2311  hba1  2330  hban  2337  hb3an  2338  nfal  2358  hbex  2360  nfsbv  2365  cbv3v  2369  cbv3  2431  equs45f  2493  nfs1  2522  sb6f  2531  hbsb  2558  hbab1  2752  nfsab  2755  nfsabg  2756  nfcrii  2922  ralrimi  3265  hbra1  3304  nfralw  3314  bnj1316  35275  bnj1379  35285  bnj1468  35301  bnj958  35395  bnj981  35405  bnj1014  35416  bnj1128  35445  bnj1204  35467  bnj1279  35473  bnj1398  35489  bnj1408  35491  bnj1444  35498  bnj1445  35499  bnj1446  35500  bnj1447  35501  bnj1448  35502  bnj1449  35503  bnj1463  35510  bnj1312  35513  bnj1518  35519  bnj1519  35520  bnj1520  35521  bnj1525  35524  bj-cbv2v  37492  bj-equs45fv  37505  mpobi123f  38871