Theorem nf5ri 2202

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

Syntax hints:   → wi 4  ∀wal 1539  Ⅎ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 1968  ax-7 2009  ax-12 2184

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

This theorem is referenced by:  19.3  2209  alimd  2219  alrimi  2220  eximd  2223  nexd  2228  albid  2229  exbid  2230  hbs1  2280  hba1  2299  hban  2306  hb3an  2307  nfal  2328  hbex  2330  nfsbv  2335  cbv3v  2339  cbv3  2401  equs45f  2463  nfs1  2492  sb6f  2501  hbsb  2528  hbab1  2723  nfsab  2726  nfsabg  2727  nfcrii  2893  ralrimi  3234  hbra1  3273  nfralw  3283  bnj1316  34976  bnj1379  34986  bnj1468  35002  bnj958  35096  bnj981  35106  bnj1014  35117  bnj1128  35146  bnj1204  35168  bnj1279  35174  bnj1398  35190  bnj1408  35192  bnj1444  35199  bnj1445  35200  bnj1446  35201  bnj1447  35202  bnj1448  35203  bnj1449  35204  bnj1463  35211  bnj1312  35214  bnj1518  35220  bnj1519  35221  bnj1520  35222  bnj1525  35225  bj-cbv2v  36999  bj-equs45fv  37012  mpobi123f  38363