Theorem hba1 698

Description: x is not free in A.xph. Appendix example in [Megill] p. 450 (p. 19 of the preprint).

Assertion

Ref	Expression
hba1	|- (A.xph -> A.xA.xph)

Proof of Theorem hba1

Step	Hyp	Ref	Expression
1		id 9	. 2 |- (A.xph -> A.xph)
2	1	a5i 687	1 |- (A.xph -> A.xA.xph)

Syntax hints:   -> wi 2  A.wal 672

This theorem is referenced by:  hbn1 708  19.12 729  19.21 738  19.38 760  19.21g 792  exintr 793  sbied 903  hbsb4t 906  ddelimf2 907  sbal1 996  hbeu1 1015  hbeu 1016  moexex 1058  2eu1 1067  2eu4 1070  hbra1 1237  ralcom2 1314  alexeq 1409  axrep 1473  axrep2 1474  zfrep2 1475  hbss 1501  moabex 1868  ssopab2 2119  dmcosseq 2572  fv3 2839  cbvfo 2923  pssnn 3428  fiint 3445  aceq1 3552  zornlem4 3606  hta 3619  axrepndlem1 3738  axrepndlem2 3739  axunnd 3742  axpowndlem2 3744  axpowndlem3 3745  axpowndlem4 3746  axregndlem2 3749  axinfndlem1 3751  axinfnd 3752  axacndlem4 3756  axacndlem5 3757  axacnd 3758  zfcndrep 3760  suppsrlem 4015  suppsr2 4017  suppsr3 4018

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-mp 6  ax-5 674  ax-gen 677

metamath.org