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

Theorem hba1 1478
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 1472 1  |-  ( A. x ph  ->  A. x A. x ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1287
This theorem was proved from axioms:  ax-ial 1472
This theorem is referenced by:  nfa1  1479  a5i  1480  hba2  1488  hbia1  1489  19.21h  1494  19.21ht  1518  exim  1535  19.12  1600  19.38  1611  ax9o  1633  equveli  1689  nfald  1690  equs5a  1722  ax11v2  1748  equs5  1757  equs5or  1758  sb56  1813  hbsb4t  1937  hbeu1  1958  eupickbi  2030  moexexdc  2032  2eu4  2041  exists2  2045  hbra1  2408
  Copyright terms: Public domain W3C validator