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

Syntax hints:   → wi 4  ∀wal 1538  Ⅎwnf 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-12 2177

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-nf 1784

This theorem is referenced by:  19.3  2202  alimd  2212  alrimi  2213  eximd  2216  nexd  2221  albid  2222  exbid  2223  hbs1  2274  hba1  2293  hban  2300  hb3an  2301  nfal  2323  hbex  2325  nfsbv  2330  cbv3v  2336  cbv3  2401  equs45f  2463  nfs1  2492  sb6f  2501  hbsb  2528  hbab1  2722  nfsab  2725  nfsabg  2726  nfcrii  2893  ralrimi  3240  hbra1  3281  nfralw  3291  bnj1316  34851  bnj1379  34861  bnj1468  34877  bnj958  34971  bnj981  34981  bnj1014  34992  bnj1128  35021  bnj1204  35043  bnj1279  35049  bnj1398  35065  bnj1408  35067  bnj1444  35074  bnj1445  35075  bnj1446  35076  bnj1447  35077  bnj1448  35078  bnj1449  35079  bnj1463  35086  bnj1312  35089  bnj1518  35095  bnj1519  35096  bnj1520  35097  bnj1525  35100  bj-cbv2v  36816  bj-equs45fv  36829  mpobi123f  38186