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

Theorem nf5rd 2104
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 2102 . 2 (Ⅎ𝑥𝜓 → (𝜓 → ∀𝑥𝜓))
31, 2syl 17 1 (𝜑 → (𝜓 → ∀𝑥𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1521  wnf 1748
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-12 2087
This theorem depends on definitions:  df-bi 197  df-ex 1745  df-nf 1750
This theorem is referenced by:  alrimdd  2121  nf5di  2157  hbimd  2164  hbnt  2182  nfaldOLD  2202  dvelimhw  2209  spimed  2291  cbv2  2306  dveeq2  2334  dveeq1  2336  axc9  2338  dvelimh  2367  abidnf  3408  eusvnfb  4892  axrepnd  9454  axacndlem4  9470  bj-spimedv  32844  bj-cbv2v  32857  wl-nfeqfb  33453
  Copyright terms: Public domain W3C validator