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

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

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