Theorem hba1 1527

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

Syntax hints:   -> wi 4   A.wal 1340

This theorem was proved from axioms:  ax-ial 1521

This theorem is referenced by:  nfa1  1528  a5i  1530  hba2  1538  hbia1  1539  19.21h  1544  19.21ht  1568  exim  1586  19.12  1652  19.38  1663  ax9o  1685  equveli  1746  nfald  1747  equs5a  1781  ax11v2  1807  equs5  1816  equs5or  1817  sb56  1872  hbsb4t  2000  hbeu1  2023  eupickbi  2095  moexexdc  2097  2eu4  2106  exists2  2110  hbra1  2494