Theorem nf5ri 2198

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 2194	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 2180

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

This theorem is referenced by:  19.3  2205  alimd  2215  alrimi  2216  eximd  2219  nexd  2224  albid  2225  exbid  2226  hbs1  2276  hba1  2295  hban  2302  hb3an  2303  nfal  2324  hbex  2326  nfsbv  2331  cbv3v  2335  cbv3  2397  equs45f  2459  nfs1  2488  sb6f  2497  hbsb  2524  hbab1  2718  nfsab  2721  nfsabg  2722  nfcrii  2889  ralrimi  3230  hbra1  3269  nfralw  3279  bnj1316  34832  bnj1379  34842  bnj1468  34858  bnj958  34952  bnj981  34962  bnj1014  34973  bnj1128  35002  bnj1204  35024  bnj1279  35030  bnj1398  35046  bnj1408  35048  bnj1444  35055  bnj1445  35056  bnj1446  35057  bnj1447  35058  bnj1448  35059  bnj1449  35060  bnj1463  35067  bnj1312  35070  bnj1518  35076  bnj1519  35077  bnj1520  35078  bnj1525  35081  bj-cbv2v  36840  bj-equs45fv  36853  mpobi123f  38210