Theorem hba1 1433

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 1427	1 |- ( A. x ph -> A. x A. x ph )

Syntax hints:   -> wi 4   A.wal 1241

This theorem was proved from axioms:  ax-ial 1427

This theorem is referenced by:  nfa1  1434  a5i  1435  hba2  1443  hbia1  1444  19.21h  1449  19.21ht  1473  exim  1490  19.12  1555  19.38  1566  ax9o  1588  equveli  1642  nfald  1643  equs5a  1675  ax11v2  1701  equs5  1710  equs5or  1711  sb56  1765  hbsb4t  1889  hbeu1  1910  eupickbi  1982  moexexdc  1984  2eu4  1993  exists2  1997  hbra1  2354