Theorem hba1 1800

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.) (Proof shortened by Wolf Lammen, 15-Dec-2017.)

Assertion

Ref	Expression
hba1	|- ( A. x ph -> A. x A. x ph )

Proof of Theorem hba1

Step	Hyp	Ref	Expression
1		alex 1578	. 2 |- ( A. x ph <-> -. E. x -. ph )
2		hbe1 1742	. . 3 |- ( E. x -. ph -> A. x E. x -. ph )
3	2	hbn 1797	. 2 |- ( -. E. x -. ph -> A. x -. E. x -. ph )
4	1, 3	hbxfrbi 1574	1 |- ( A. x ph -> A. x A. x ph )

Syntax hints:   -. wn 3   -> wi 4   A.wal 1546   E.wex 1547

This theorem is referenced by:  nfa1  1802  spimehOLD  1836  19.21hOLD  1858  19.12OLD  1866  nfald  1867  cbv3hvOLD  1875  ax12olem5OLD  1981  ax10lem4OLD  1996  ax9OLD  1999  dvelimhOLD  2016  axi5r  2376  axial  2377  hbra1  2715  hbntal  28351  hbimpg  28352  hbimpgVD  28725  hbalgVD  28726  hbexgVD  28727  a9e2eqVD  28728  e2ebindVD  28733  vk15.4jVD  28735  cbv3hvNEW7  29152  19.12vAUX7  29160  ax9NEW7  29174  ax10lem4NEW7  29177  dvelimhvAUX7  29198  dral1NEW7  29199  equs5NEW7  29238  ax7w1AUX7  29345  ax7w4AUX7  29358  19.12OLD7  29370  dvelimhOLD7  29397

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-11 1757

This theorem depends on definitions:  df-bi 178  df-ex 1548