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

Theorem nf5rd 2189
 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 2185 . 2 (Ⅎ𝑥𝜓 → (𝜓 → ∀𝑥𝜓))
31, 2syl 17 1 (𝜑 → (𝜓 → ∀𝑥𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∀wal 1528  Ⅎwnf 1777 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-12 2169 This theorem depends on definitions:  df-bi 208  df-ex 1774  df-nf 1778 This theorem is referenced by:  spimedv  2190  alrimdd  2207  nf5di  2287  hbnt  2296  hbimd  2300  dvelimhw  2360  dveeq2  2391  dveeq1  2393  axc9  2395  spimed  2402  cbv2OLD  2423  dvelimh  2469  abidnf  3698  eusvnfb  5290  axrepnd  10010  axacndlem4  10026  bj-cbv2v  34023  wl-nfeqfb  34663
 Copyright terms: Public domain W3C validator