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

Ref  Expression 

hbth.1 
Ref  Expression 

hbth 
Step  Hyp  Ref  Expression 

1  hbth.1  . . 3  
2  1  axgen 1618  . 2 
3  2  a1i 11  1 
Colors of variables: wff setvar class 
Syntax hints: > wi 4 A. wal 1393 
This theorem is referenced by: nfth 1625 spfalw 1786 
This theorem was proved from axioms: axmp 5 ax1 6 axgen 1618 
Copyright terms: Public domain  W3C validator 