Theorem nf5ri 2186

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

Syntax hints:   → wi 4  ∀wal 1537  Ⅎ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 1911  ax-6 1969  ax-7 2009  ax-12 2169

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

This theorem is referenced by:  19.3  2193  alimd  2203  alrimi  2204  eximd  2207  nexd  2212  albid  2213  exbid  2214  hbs1  2263  hba1  2287  hban  2294  hb3an  2295  nfal  2314  hbex  2316  nfsbv  2321  hbsbwOLD  2323  cbv3v  2329  cbv3  2394  equs45f  2456  nfs1  2485  sb6f  2494  hbsb  2521  hbab1  2716  nfsab  2720  nfsabg  2721  nfcrii  2893  nfcriiOLD  2894  ralrimi  3252  hbra1  3296  nfralw  3306  bnj1316  34127  bnj1379  34137  bnj1468  34153  bnj958  34247  bnj981  34257  bnj1014  34268  bnj1128  34297  bnj1204  34319  bnj1279  34325  bnj1398  34341  bnj1408  34343  bnj1444  34350  bnj1445  34351  bnj1446  34352  bnj1447  34353  bnj1448  34354  bnj1449  34355  bnj1463  34362  bnj1312  34365  bnj1518  34371  bnj1519  34372  bnj1520  34373  bnj1525  34376  bj-cbv2v  35981  bj-equs45fv  35994  mpobi123f  37335