Theorem nf5ri 2204

Description: Consequence of the definition of not-free. (Contributed by Mario Carneiro, 11-Aug-2016.)

Hypothesis

Ref	Expression
nf5ri.1	⊢ Ⅎ𝑥𝜑

Assertion

Ref	Expression
nf5ri	⊢ (𝜑 → ∀𝑥𝜑)

Proof of Theorem nf5ri

Step	Hyp	Ref	Expression
1		nf5ri.1	. 2 ⊢ Ⅎ𝑥𝜑
2		nf5r 2203	. 2 ⊢ (Ⅎ𝑥𝜑 → (𝜑 → ∀𝑥𝜑))
3	1, 2	ax-mp 5	1 ⊢ (𝜑 → ∀𝑥𝜑)

Syntax hints:   → wi 4  ∀wal 1622  Ⅎwnf 1849

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-12 2188

This theorem depends on definitions:  df-bi 197  df-ex 1846  df-nf 1851

This theorem is referenced by:  19.3  2208  alimd  2220  alrimi  2221  eximd  2224  nexd  2228  albid  2229  exbid  2230  hban  2267  hb3an  2268  hba1  2290  nfal  2292  nfexOLD  2294  hbex  2295  cbv2  2407  equs45f  2479  nfs1  2494  sb6f  2514  hbsb  2570  nfsab  2744  nfcrii  2887  hbra1  3072  ralrimi  3087  bnj1316  31190  bnj1379  31200  bnj1468  31215  bnj958  31309  bnj981  31319  bnj1014  31329  bnj1128  31357  bnj1204  31379  bnj1279  31385  bnj1398  31401  bnj1408  31403  bnj1444  31410  bnj1445  31411  bnj1446  31412  bnj1447  31413  bnj1448  31414  bnj1449  31415  bnj1463  31422  bnj1312  31425  bnj1518  31431  bnj1519  31432  bnj1520  31433  bnj1525  31436  bj-cbv2v  33030  bj-equs45fv  33050  bj-nfcrii  33149  mpt2bi123f  34276