Theorem nf5ri 2235

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1568  Ⅎwnf 1816

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-12 2216

This proof depends on definitions:  df-bi 210  df-ex 1813  df-nf 1817

This theorem is used by:  19.3  2242  alimd  2252  alrimi  2253  eximd  2256  nexd  2261  albid  2262  exbid  2263  hbs1  2311  hba1  2330  hbanOLD  2337  hb3anOLD  2338  nfal  2357  hbex  2359  nfsbv  2364  cbv3v  2368  cbv3  2429  equs45f  2491  nfs1  2520  sb6f  2529  hbsb  2556  hbab1  2750  nfsab  2753  nfsabg  2754  nfcrii  2921  ralrimi  3264  hbra1  3303  nfralw  3313  bnj1316  35561  bnj1379  35571  bnj1468  35587  bnj958  35681  bnj981  35691  bnj1014  35702  bnj1128  35731  bnj1204  35753  bnj1279  35759  bnj1398  35775  bnj1408  35777  bnj1444  35784  bnj1445  35785  bnj1446  35786  bnj1447  35787  bnj1448  35788  bnj1449  35789  bnj1463  35796  bnj1312  35799  bnj1518  35805  bnj1519  35806  bnj1520  35807  bnj1525  35810  bj-cbv2v  37925  bj-equs45fv  37938  mpobi123f  39360