Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > hbth  Unicode 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 from smaller formulas of this form. These are useful for constructing hypotheses that state " is (effectively) not free in ." (Contributed by NM, 5Aug1993.) 
Ref  Expression 

hbth.1 
Ref  Expression 

hbth 
Step  Hyp  Ref  Expression 

1  hbth.1  . . 3  
2  1  axgen 1546  . 2 
3  2  a1i 10  1 
Colors of variables: wff set class 
Syntax hints: wi 4 wal 1540 
This theorem is referenced by: nfth 1553 spfalw 1672 spimehOLD 1823 ax9lem12 29220 ax9lem13 29221 
This theorem was proved from axioms: ax1 5 axmp 8 axgen 1546 
Copyright terms: Public domain  W3C validator 