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

Theorem hbe1 1365
Description: x is not free in xφ. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
hbe1 (xφxxφ)

Proof of Theorem hbe1
StepHypRef Expression
1 ax-ie1 1363 1 (xφxxφ)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1226  wex 1362
This theorem was proved from axioms:  ax-ie1 1363
This theorem is referenced by:  nfe1  1366  19.8a  1464  exim  1472  19.43  1501  hbex  1509  excomim  1535  19.38  1548  exan  1565  equs5e  1658  exdistrfor  1663  hbmo1  1920  euan  1938  euor2  1940  eupicka  1962  mopick2  1965  moexexdc  1966  2moex  1968  2euex  1969  2exeu  1974  2eu4  1975  2eu7  1976
  Copyright terms: Public domain W3C validator