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

Theorem nf5ri 2053
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 2052 . 2 (Ⅎ𝑥𝜑 → (𝜑 → ∀𝑥𝜑))
31, 2ax-mp 5 1 (𝜑 → ∀𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1473  wnf 1699
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034
This theorem depends on definitions:  df-bi 196  df-ex 1696  df-nf 1701
This theorem is referenced by:  19.3  2057  alimd  2068  alrimi  2069  eximd  2072  nexd  2076  albid  2077  exbid  2078  hban  2113  hb3an  2114  hba1  2137  nfal  2139  nfexOLD  2141  hbex  2142  cbv2  2258  equs45f  2338  nfs1  2353  sb6f  2373  hbsb  2429  nfsab  2602  nfcrii  2744  hbra1  2926  ralrimi  2940  bnj1316  30145  bnj1379  30155  bnj1468  30170  bnj958  30264  bnj981  30274  bnj1014  30284  bnj1128  30312  bnj1204  30334  bnj1279  30340  bnj1398  30356  bnj1408  30358  bnj1444  30365  bnj1445  30366  bnj1446  30367  bnj1447  30368  bnj1448  30369  bnj1449  30370  bnj1463  30377  bnj1312  30380  bnj1518  30386  bnj1519  30387  bnj1520  30388  bnj1525  30391  bj-cbv2v  31919  bj-equs45fv  31940  bj-nfcrii  32045  mpt2bi123f  33141
  Copyright terms: Public domain W3C validator