Theorem nf5ri 2191

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

Syntax hints:   → wi 4  ∀wal 1539  Ⅎwnf 1789

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-12 2174

This theorem depends on definitions:  df-bi 206  df-ex 1786  df-nf 1790

This theorem is referenced by:  19.3  2198  alimd  2208  alrimi  2209  eximd  2212  nexd  2217  albid  2218  exbid  2219  hbs1  2269  hba1  2293  hban  2300  hb3an  2301  nfal  2320  hbex  2322  nfsbv  2327  hbsbwOLD  2329  cbv3v  2335  cbv3  2398  equs45f  2460  nfs1  2493  sb6f  2502  hbsb  2530  hbab1  2725  nfsab  2729  nfsabg  2730  nfcrii  2900  nfcriiOLD  2901  ralrimi  3141  hbra1  3145  bnj1316  32779  bnj1379  32789  bnj1468  32805  bnj958  32899  bnj981  32909  bnj1014  32920  bnj1128  32949  bnj1204  32971  bnj1279  32977  bnj1398  32993  bnj1408  32995  bnj1444  33002  bnj1445  33003  bnj1446  33004  bnj1447  33005  bnj1448  33006  bnj1449  33007  bnj1463  33014  bnj1312  33017  bnj1518  33023  bnj1519  33024  bnj1520  33025  bnj1525  33028  bj-cbv2v  34959  bj-equs45fv  34972  mpobi123f  36299