Theorem nf5ri 2230

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 2229	. 2 ⊢ (Ⅎ𝑥𝜑 → (𝜑 → ∀𝑥𝜑))
3	1, 2	ax-mp 5	1 ⊢ (𝜑 → ∀𝑥𝜑)

Syntax hints:   → wi 4  ∀wal 1635  Ⅎwnf 1863

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-12 2214

This theorem depends on definitions:  df-bi 198  df-ex 1860  df-nf 1864

This theorem is referenced by:  19.3  2235  alimd  2248  alrimi  2249  eximd  2252  nexd  2257  albid  2258  exbid  2259  hbs1  2287  hban  2304  hb3an  2305  hba1  2327  nfal  2329  nfexOLD  2331  hbex  2332  cbv2  2443  equs45f  2508  nfs1  2524  sb6f  2544  hbsb  2603  nfsab  2798  nfcrii  2941  hbra1  3130  ralrimi  3145  bnj1316  31214  bnj1379  31224  bnj1468  31239  bnj958  31333  bnj981  31343  bnj1014  31353  bnj1128  31381  bnj1204  31403  bnj1279  31409  bnj1398  31425  bnj1408  31427  bnj1444  31434  bnj1445  31435  bnj1446  31436  bnj1447  31437  bnj1448  31438  bnj1449  31439  bnj1463  31446  bnj1312  31449  bnj1518  31455  bnj1519  31456  bnj1520  31457  bnj1525  31460  bj-cbv2v  33046  bj-equs45fv  33066  mpt2bi123f  34281