MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nf5ri Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 nf5ri.1 . 2 𝑥𝜑
2 nf5r 2203 . 2 (Ⅎ𝑥𝜑 → (𝜑 → ∀𝑥𝜑))
31, 2ax-mp 5 1 (𝜑 → ∀𝑥𝜑)
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator