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

Theorem nf5ri 2063
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 2062 . 2 (Ⅎ𝑥𝜑 → (𝜑 → ∀𝑥𝜑))
31, 2ax-mp 5 1 (𝜑 → ∀𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1479  wnf 1706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-12 2045
This theorem depends on definitions:  df-bi 197  df-ex 1703  df-nf 1708
This theorem is referenced by:  19.3  2067  alimd  2079  alrimi  2080  eximd  2083  nexd  2087  albid  2088  exbid  2089  hban  2126  hb3an  2127  hba1  2149  nfal  2151  nfexOLD  2153  hbex  2154  cbv2  2268  equs45f  2348  nfs1  2363  sb6f  2383  hbsb  2439  nfsab  2612  nfcrii  2755  hbra1  2939  ralrimi  2954  bnj1316  30865  bnj1379  30875  bnj1468  30890  bnj958  30984  bnj981  30994  bnj1014  31004  bnj1128  31032  bnj1204  31054  bnj1279  31060  bnj1398  31076  bnj1408  31078  bnj1444  31085  bnj1445  31086  bnj1446  31087  bnj1447  31088  bnj1448  31089  bnj1449  31090  bnj1463  31097  bnj1312  31100  bnj1518  31106  bnj1519  31107  bnj1520  31108  bnj1525  31111  bj-cbv2v  32707  bj-equs45fv  32727  bj-nfcrii  32826  mpt2bi123f  33942
  Copyright terms: Public domain W3C validator