Theorem nf5ri 2195

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 2190	1 ⊢ (𝜑 → ∀𝑥𝜑)

Syntax hints:   → wi 4  ∀wal 1535  Ⅎ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 1970  ax-7 2015  ax-12 2177

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

This theorem is referenced by:  19.3  2202  alimd  2212  alrimi  2213  eximd  2216  nexd  2223  albid  2224  exbid  2225  hbs1  2274  sbbibOLD  2289  hba1  2301  hban  2308  hb3an  2309  nfal  2342  hbex  2344  hbsbw  2351  cbv3v  2355  cbv3  2415  cbv2OLD  2427  equs45f  2482  nfs1  2527  sb6f  2537  hbsb  2567  sb6fALT  2602  nfsab  2812  nfsabg  2813  nfcrii  2970  ralrimi  3216  hbra1  3220  bnj1316  32092  bnj1379  32102  bnj1468  32118  bnj958  32212  bnj981  32222  bnj1014  32233  bnj1128  32262  bnj1204  32284  bnj1279  32290  bnj1398  32306  bnj1408  32308  bnj1444  32315  bnj1445  32316  bnj1446  32317  bnj1447  32318  bnj1448  32319  bnj1449  32320  bnj1463  32327  bnj1312  32330  bnj1518  32336  bnj1519  32337  bnj1520  32338  bnj1525  32341  bj-cbv2v  34120  bj-equs45fv  34133  mpobi123f  35455