ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  hbth GIF version

Theorem hbth 1352
Description: No variable is (effectively) free in a theorem.

This and later "hypothesis-building" 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, 5-Aug-1993.)

Hypothesis
Ref Expression
hbth.1 φ
Assertion
Ref Expression
hbth (φxφ)

Proof of Theorem hbth
StepHypRef Expression
1 hbth.1 . . 3 φ
21ax-gen 1338 . 2 xφ
32a1i 9 1 (φxφ)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1241
This theorem was proved from axioms:  ax-1 5  ax-mp 7  ax-gen 1338
This theorem is referenced by:  nfth  1353  sbieh  1673  bj-sbimeh  9355
  Copyright terms: Public domain W3C validator