Theorem hba1 1563

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

Step	Hyp	Ref	Expression
1		ax-ial 1557	1 |- ( A. x ph -> A. x A. x ph )

Syntax hints:   -> wi 4   A.wal 1371

This theorem was proved from axioms:  ax-ial 1557

This theorem is referenced by:  nfa1  1564  a5i  1566  hba2  1574  hbia1  1575  19.21h  1580  19.21ht  1604  exim  1622  19.12  1688  19.38  1699  ax9o  1721  equveli  1782  nfald  1783  equs5a  1817  ax11v2  1843  equs5  1852  equs5or  1853  sb56  1909  hbsb4t  2041  hbeu1  2064  eupickbi  2136  moexexdc  2138  2eu4  2147  exists2  2151  hbra1  2536