Theorem hba1 1002

Description: x is not free in A.xph. Example in Appendix in [Megill] p. 450 (p. 19 of the preprint). Also Lemma 22 of [Monk2] p. 114.

Assertion

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

Proof of Theorem hba1

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

Syntax hints:   -> wi 3  A.wal 953

This theorem is referenced by:  hba2 1012  hbia1 1013  hbn1 1014  ax67to6 1020  ax467to6 1024  19.12 1046  19.21 1055  19.38 1080  19.21t 1114  19.23t 1115  exintr 1116  dvelimfALT 1152  sbf2 1186  sbied 1194  equs5a 1196  ax11v2 1214  equs5 1220  hbsb4t 1248  sb56 1265  sbal1 1345  dvelimALT 1352  ax11eq 1362  ax11el 1363  ax11indalem 1367  ax11inda2ALT 1368  ax11inda 1370  a12study 1377  a12studyALT 1378  hbeu1 1387  hbeu 1388  moexex 1437  2eu1 1448  2eu4 1451  hbra1 1685  ralcom2 1774  abidhb 1909  hbeqd 1910  hbeld 1911  hbsbc1gd 1980  hbsbcgd 1981  sbcralt 1987  sbcrext 1988  sbcralgf 1989  sbcrexgf 1990  csbie2t 2030  csbnestglem 2032  csbnestg 2033  csbnest1g 2034  sbcnestg 2035  hbss 2059  hbopd 2494  intab 2556  hbbrd 2655  axrep1 2690  axrep2 2691  axrep3 2692  axrep4 2693  moabex 2762  mosubopt 2800  ssopab2 2818  alxfr 2892  dmcosseq 3361  hbimad 3408  hbfvd 3725  hbfvd2 3726  fv3 3728  cbvfo 3880  hboprd 3977  fnoprabg 4007  pssnn 4522  fiint 4543  hta 4711  aceq1 4712  zorn2lem4 4774  axrepndlem1 4927  axrepndlem2 4928  axunnd 4931  axpowndlem2 4933  axpowndlem3 4934  axpowndlem4 4935  axregndlem2 4938  axinfndlem1 4940  axinfnd 4941  axacndlem4 4945  axacndlem5 4946  axacnd 4947  zfcndrep 4949  suppsrlem 5204  suppsr2 5206  suppsr3 5207  hbnegd 5346  islp2 7707  cncnplem2 7735  qusp 10489

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7  ax-gen 962  ax-5o 974

Copyright terms: Public domain