Theorem nf5ri 2196

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

Syntax hints:   → wi 4  ∀wal 1535  Ⅎwnf 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-ex 1778  df-nf 1782

This theorem is referenced by:  19.3  2203  alimd  2213  alrimi  2214  eximd  2217  nexd  2222  albid  2223  exbid  2224  hbs1  2275  hba1  2297  hban  2304  hb3an  2305  nfal  2327  hbex  2329  nfsbv  2334  cbv3v  2341  cbv3  2405  equs45f  2467  nfs1  2496  sb6f  2505  hbsb  2532  hbab1  2726  nfsab  2730  nfsabg  2731  nfcrii  2903  ralrimi  3263  hbra1  3307  nfralw  3317  bnj1316  34796  bnj1379  34806  bnj1468  34822  bnj958  34916  bnj981  34926  bnj1014  34937  bnj1128  34966  bnj1204  34988  bnj1279  34994  bnj1398  35010  bnj1408  35012  bnj1444  35019  bnj1445  35020  bnj1446  35021  bnj1447  35022  bnj1448  35023  bnj1449  35024  bnj1463  35031  bnj1312  35034  bnj1518  35040  bnj1519  35041  bnj1520  35042  bnj1525  35045  bj-cbv2v  36764  bj-equs45fv  36777  mpobi123f  38122