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

Theorem hbth 1349
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 1335 . 2 xφ
32a1i 9 1 (φxφ)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1240
This theorem was proved from axioms:  ax-1 5  ax-mp 7  ax-gen 1335
This theorem is referenced by:  nfth  1350  sbieh  1670  bj-sbimeh  9247
  Copyright terms: Public domain W3C validator