Theorem nf5ri 2231

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

Syntax hints:   → wi 4  ∀wal 1568  Ⅎwnf 1813

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-12 2213

This theorem depends on definitions:  df-bi 210  df-ex 1810  df-nf 1814

This theorem is referenced by:  19.3  2238  alimd  2248  alrimi  2249  eximd  2252  nexd  2257  albid  2258  exbid  2259  hbs1  2309  hba1  2328  hban  2335  hb3an  2336  nfal  2356  hbex  2358  nfsbv  2363  cbv3v  2367  cbv3  2429  equs45f  2491  nfs1  2520  sb6f  2529  hbsb  2556  hbab1  2750  nfsab  2753  nfsabg  2754  nfcrii  2920  ralrimi  3263  hbra1  3302  nfralw  3312  bnj1316  35208  bnj1379  35218  bnj1468  35234  bnj958  35328  bnj981  35338  bnj1014  35349  bnj1128  35378  bnj1204  35400  bnj1279  35406  bnj1398  35422  bnj1408  35424  bnj1444  35431  bnj1445  35432  bnj1446  35433  bnj1447  35434  bnj1448  35435  bnj1449  35436  bnj1463  35443  bnj1312  35446  bnj1518  35452  bnj1519  35453  bnj1520  35454  bnj1525  35457  bj-cbv2v  37453  bj-equs45fv  37466  mpobi123f  38831