Theorem hba1 1000

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

Syntax hints:   -> wi 3  A.wal 951

This theorem is referenced by:  hba2 1010  hbn1 1011  ax67to6 1017  ax467to6 1021  19.12 1043  19.21 1052  19.38 1077  19.21t 1111  19.23t 1112  exintr 1113  dvelimfALT 1149  sbf2 1183  sbied 1191  equs5a 1193  ax11v2 1210  equs5 1216  hbsb4t 1244  sb56 1261  sbal1 1341  ax11eq 1356  ax11el 1357  ax11indalem 1361  ax11inda2ALT 1362  ax11inda 1364  a12study 1371  a12studyALT 1372  hbeu1 1381  hbeu 1382  moexex 1431  2eu1 1442  2eu4 1445  hbra1 1679  ralcom2 1768  abidhb 1903  hbeqd 1904  hbeld 1905  hbsbc1gd 1973  hbsbcgd 1974  sbcralt 1980  sbcrext 1981  sbcralgf 1982  sbcrexgf 1983  csbie2t 2023  csbnestglem 2025  csbnestg 2026  csbnest1g 2027  sbcnestg 2028  hbss 2052  hbopd 2488  intab 2550  hbbrd 2649  axrep1 2684  axrep2 2685  axrep3 2686  axrep4 2687  moabex 2756  mosubopt 2793  ssopab2 2811  alxfr 2886  dmcosseq 3349  hbimad 3396  hbfvd 3715  hbfvd2 3716  fv3 3718  cbvfo 3870  hboprd 3967  fnoprabg 3997  pssnn 4513  fiint 4534  hta 4700  aceq1 4701  zorn2lem4 4763  axrepndlem1 4916  axrepndlem2 4917  axunnd 4920  axpowndlem2 4922  axpowndlem3 4923  axpowndlem4 4924  axregndlem2 4927  axinfndlem1 4929  axinfnd 4930  axacndlem4 4934  axacndlem5 4935  axacnd 4936  zfcndrep 4938  suppsrlem 5193  suppsr2 5195  suppsr3 5196  hbnegd 5335  islp2 7688  cncnplem2 7714  qusp 10430

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

Copyright terms: Public domain