Theorem hba1 1035

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 1021	1 |- (A.xph -> A.xA.xph)

Syntax hints:   -> wi 3  A.wal 986

This theorem is referenced by:  hba2 1045  hbia1 1046  hbn1 1047  ax67to6 1053  ax467to6 1057  19.12 1079  19.21 1088  19.38 1113  19.21t 1147  19.23t 1148  exintr 1149  dvelimfALT 1186  sbf2 1220  sbied 1228  equs5a 1230  ax11v2 1248  equs5 1254  hbsb4t 1282  sb56 1299  sbal1 1379  dvelimALT 1386  ax11eq 1396  ax11el 1397  ax11indalem 1401  ax11inda2ALT 1402  ax11inda 1404  a12study 1411  a12studyALT 1412  hbeu1 1421  hbeu 1422  moexex 1472  2eu1 1483  2eu4 1486  hbra1 1725  ralcom2 1814  abidhb 1950  hbeqd 1951  hbeld 1952  hbsbc1gd 2023  hbsbcgd 2024  sbcralt 2032  sbcrext 2033  sbcralgf 2034  sbcrexgf 2035  csbie2t 2077  csbnestglem 2079  csbnestg 2080  csbnest1g 2081  sbcnestg 2082  hbss 2106  hbopd 2545  intab 2608  hbbrd 2709  axrep1 2745  axrep2 2746  axrep3 2747  axrep4 2748  moabex 2819  mosubopt 2857  ssopab2 2876  alxfr 2951  dmcosseq 3425  hbimad 3475  hbfvd 3806  hbfvd2 3807  fv3 3809  cbvfo 3961  hboprd 4058  fnoprabg 4089  pssnn 4623  fiint 4644  hta 4814  aceq1 4815  zorn2lem4 4877  axrepndlem1 5033  axrepndlem2 5034  axunnd 5037  axpowndlem2 5039  axpowndlem3 5040  axpowndlem4 5041  axregndlem2 5044  axinfndlem1 5046  axinfnd 5047  axacndlem4 5051  axacndlem5 5052  axacnd 5053  zfcndrep 5055  suppsrlem 5310  suppsr2 5312  suppsr3 5313  hbnegd 5452  islp2 7867  cncnplem2 7895  qusp 10694

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

Copyright terms: Public domain