Theorem nf5ri 2189

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

Syntax hints:   → wi 4  ∀wal 1540  Ⅎwnf 1786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2172

This theorem depends on definitions:  df-bi 206  df-ex 1783  df-nf 1787

This theorem is referenced by:  19.3  2196  alimd  2206  alrimi  2207  eximd  2210  nexd  2215  albid  2216  exbid  2217  hbs1  2266  hba1  2290  hban  2297  hb3an  2298  nfal  2317  hbex  2319  nfsbv  2324  hbsbwOLD  2326  cbv3v  2332  cbv3  2397  equs45f  2459  nfs1  2488  sb6f  2497  hbsb  2524  hbab1  2719  nfsab  2723  nfsabg  2724  nfcrii  2896  nfcriiOLD  2897  ralrimi  3255  hbra1  3299  nfralw  3309  bnj1316  33820  bnj1379  33830  bnj1468  33846  bnj958  33940  bnj981  33950  bnj1014  33961  bnj1128  33990  bnj1204  34012  bnj1279  34018  bnj1398  34034  bnj1408  34036  bnj1444  34043  bnj1445  34044  bnj1446  34045  bnj1447  34046  bnj1448  34047  bnj1449  34048  bnj1463  34055  bnj1312  34058  bnj1518  34064  bnj1519  34065  bnj1520  34066  bnj1525  34069  bj-cbv2v  35665  bj-equs45fv  35678  mpobi123f  37019