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

Theorem hba1 1430
Description: x is not free in xφ. Example in Appendix in [Megill] p. 450 (p. 19 of the preprint). Also Lemma 22 of [Monk2] p. 114. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
hba1 (xφxxφ)

Proof of Theorem hba1
StepHypRef Expression
1 ax-ial 1424 1 (xφxxφ)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1240
This theorem was proved from axioms:  ax-ial 1424
This theorem is referenced by:  nfa1  1431  a5i  1432  hba2  1440  hbia1  1441  19.21h  1446  19.21ht  1470  exim  1487  19.12  1552  19.38  1563  ax9o  1585  equveli  1639  nfald  1640  equs5a  1672  ax11v2  1698  equs5  1707  equs5or  1708  sb56  1762  hbsb4t  1886  hbeu1  1907  eupickbi  1979  moexexdc  1981  2eu4  1990  exists2  1994  hbra1  2348
  Copyright terms: Public domain W3C validator