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

Theorem hba1 1551
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 1545 1  |-  ( A. x ph  ->  A. x A. x ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1362
This theorem was proved from axioms:  ax-ial 1545
This theorem is referenced by:  nfa1  1552  a5i  1554  hba2  1562  hbia1  1563  19.21h  1568  19.21ht  1592  exim  1610  19.12  1676  19.38  1687  ax9o  1709  equveli  1770  nfald  1771  equs5a  1805  ax11v2  1831  equs5  1840  equs5or  1841  sb56  1897  hbsb4t  2025  hbeu1  2048  eupickbi  2120  moexexdc  2122  2eu4  2131  exists2  2135  hbra1  2520
  Copyright terms: Public domain W3C validator