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

Theorem hba1 1521
Description:  x is not free in  A. x ph. 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  |-  ( A. x ph  ->  A. x A. x ph )

Proof of Theorem hba1
StepHypRef Expression
1 ax-ial 1515 1  |-  ( A. x ph  ->  A. x A. x ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1330
This theorem was proved from axioms:  ax-ial 1515
This theorem is referenced by:  nfa1  1522  a5i  1523  hba2  1531  hbia1  1532  19.21h  1537  19.21ht  1561  exim  1579  19.12  1644  19.38  1655  ax9o  1677  equveli  1733  nfald  1734  equs5a  1767  ax11v2  1793  equs5  1802  equs5or  1803  sb56  1858  hbsb4t  1989  hbeu1  2010  eupickbi  2082  moexexdc  2084  2eu4  2093  exists2  2097  hbra1  2468
  Copyright terms: Public domain W3C validator