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

Theorem nf5rd 2054
 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 2052 . 2 (Ⅎ𝑥𝜓 → (𝜓 → ∀𝑥𝜓))
31, 2syl 17 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:  alrimdd  2070  nf5di  2105  hbimd  2111  hbnt  2129  nfaldOLD  2152  dvelimhw  2159  spimed  2243  cbv2  2258  dveeq2  2286  dveeq1  2288  axc9  2290  dvelimh  2324  abidnf  3342  eusvnfb  4788  axrepnd  9295  axacndlem4  9311  bj-spimedv  31906  bj-cbv2v  31919  wl-nfeqfb  32502
 Copyright terms: Public domain W3C validator