Intuitionistic Logic Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > ILE Home > Th. List > hbth  Structured version GIF version 
Description: No variable is
(effectively) free in a theorem.
This and later "hypothesisbuilding" lemmas, with labels starting "hb...", allow us to construct proofs of formulas of the form ⊢ (φ → ∀xφ) from smaller formulas of this form. These are useful for constructing hypotheses that state "x is (effectively) not free in φ." (Contributed by NM, 5Aug1993.) 
Ref  Expression 

hbth.1  ⊢ φ 
Ref  Expression 

hbth  ⊢ (φ → ∀xφ) 
Step  Hyp  Ref  Expression 

1  hbth.1  . . 3 ⊢ φ  
2  1  axgen 1335  . 2 ⊢ ∀xφ 
3  2  a1i 9  1 ⊢ (φ → ∀xφ) 
Colors of variables: wff set class 
Syntax hints: → wi 4 ∀wal 1240 
This theorem was proved from axioms: ax1 5 axmp 7 axgen 1335 
This theorem is referenced by: nfth 1350 sbieh 1670 bjsbimeh 9247 
Copyright terms: Public domain  W3C validator 