Theorem nf5ri 2193

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

Syntax hints:   → wi 4  ∀wal 1536  Ⅎwnf 1785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-12 2175

This theorem depends on definitions:  df-bi 210  df-ex 1782  df-nf 1786

This theorem is referenced by:  19.3  2200  alimd  2210  alrimi  2211  eximd  2214  nexd  2221  albid  2222  exbid  2223  hbs1  2271  sbbibOLD  2285  hba1  2297  hban  2304  hb3an  2305  nfal  2331  hbex  2333  hbsbwOLD  2340  cbv3v  2344  cbv3  2404  cbv2OLD  2416  equs45f  2471  nfs1  2506  sb6f  2515  hbsb  2544  sb6fALT  2578  nfsab  2789  nfsabg  2790  nfcrii  2948  nfcriiOLD  2949  ralrimi  3180  hbra1  3184  bnj1316  32202  bnj1379  32212  bnj1468  32228  bnj958  32322  bnj981  32332  bnj1014  32343  bnj1128  32372  bnj1204  32394  bnj1279  32400  bnj1398  32416  bnj1408  32418  bnj1444  32425  bnj1445  32426  bnj1446  32427  bnj1447  32428  bnj1448  32429  bnj1449  32430  bnj1463  32437  bnj1312  32440  bnj1518  32446  bnj1519  32447  bnj1520  32448  bnj1525  32451  bj-cbv2v  34235  bj-equs45fv  34248  mpobi123f  35600