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

Theorem nf5rd 2190
Description: Consequence of the definition of not-free in a context. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypothesis
Ref Expression
nf5rd.1 (𝜑 → Ⅎ𝑥𝜓)
Assertion
Ref Expression
nf5rd (𝜑 → (𝜓 → ∀𝑥𝜓))

Proof of Theorem nf5rd
StepHypRef Expression
1 nf5rd.1 . 2 (𝜑 → Ⅎ𝑥𝜓)
2 nf5r 2188 . 2 (Ⅎ𝑥𝜓 → (𝜓 → ∀𝑥𝜓))
31, 2syl 17 1 (𝜑 → (𝜓 → ∀𝑥𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1540  wnf 1786
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2172
This theorem depends on definitions:  df-bi 206  df-ex 1783  df-nf 1787
This theorem is referenced by:  spimedv  2191  alrimdd  2208  nf5di  2282  hbnt  2291  hbimd  2295  dvelimhw  2342  dveeq2  2378  dveeq1  2380  axc9  2382  spimed  2388  dvelimh  2450  abidnf  3699  eusvnfb  5392  axrepnd  10589  axacndlem4  10605  bj-cbv2v  35676  bj-elgab  35819  wl-nfeqfb  36405
  Copyright terms: Public domain W3C validator