Theorem nf5ri 2183

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

Syntax hints:   → wi 4  ∀wal 1531  Ⅎwnf 1777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-12 2166

This theorem depends on definitions:  df-bi 206  df-ex 1774  df-nf 1778

This theorem is referenced by:  19.3  2190  alimd  2200  alrimi  2201  eximd  2204  nexd  2209  albid  2210  exbid  2211  hbs1  2260  hba1  2282  hban  2289  hb3an  2290  nfal  2311  hbex  2313  nfsbv  2318  cbv3v  2325  cbv3  2390  equs45f  2452  nfs1  2481  sb6f  2490  hbsb  2517  hbab1  2711  nfsab  2715  nfsabg  2716  nfcrii  2885  ralrimi  3244  hbra1  3288  nfralw  3298  bnj1316  34582  bnj1379  34592  bnj1468  34608  bnj958  34702  bnj981  34712  bnj1014  34723  bnj1128  34752  bnj1204  34774  bnj1279  34780  bnj1398  34796  bnj1408  34798  bnj1444  34805  bnj1445  34806  bnj1446  34807  bnj1447  34808  bnj1448  34809  bnj1449  34810  bnj1463  34817  bnj1312  34820  bnj1518  34826  bnj1519  34827  bnj1520  34828  bnj1525  34831  bj-cbv2v  36406  bj-equs45fv  36419  mpobi123f  37766