Theorem hba1 1003

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

Syntax hints:   -> wi 3  A.wal 954

This theorem is referenced by:  hba2 1013  hbia1 1014  hbn1 1015  ax67to6 1021  ax467to6 1025  19.12 1047  19.21 1056  19.38 1081  19.21t 1115  19.23t 1116  exintr 1117  dvelimfALT 1153  sbf2 1187  sbied 1195  equs5a 1197  ax11v2 1215  equs5 1221  hbsb4t 1249  sb56 1266  sbal1 1346  dvelimALT 1353  ax11eq 1363  ax11el 1364  ax11indalem 1368  ax11inda2ALT 1369  ax11inda 1371  a12study 1378  a12studyALT 1379  hbeu1 1388  hbeu 1389  moexex 1438  2eu1 1449  2eu4 1452  hbra1 1687  ralcom2 1776  abidhb 1912  hbeqd 1913  hbeld 1914  hbsbc1gd 1983  hbsbcgd 1984  sbcralt 1990  sbcrext 1991  sbcralgf 1992  sbcrexgf 1993  csbie2t 2033  csbnestglem 2035  csbnestg 2036  csbnest1g 2037  sbcnestg 2038  hbss 2062  hbopd 2497  intab 2560  hbbrd 2659  axrep1 2694  axrep2 2695  axrep3 2696  axrep4 2697  moabex 2766  mosubopt 2804  ssopab2 2822  alxfr 2896  dmcosseq 3365  hbimad 3412  hbfvd 3730  hbfvd2 3731  fv3 3733  cbvfo 3885  hboprd 3982  fnoprabg 4012  pssnn 4534  fiint 4559  fiintOLD 4560  hta 4728  aceq1 4729  zorn2lem4 4791  axrepndlem1 4944  axrepndlem2 4945  axunnd 4948  axpowndlem2 4950  axpowndlem3 4951  axpowndlem4 4952  axregndlem2 4955  axinfndlem1 4957  axinfnd 4958  axacndlem4 4962  axacndlem5 4963  axacnd 4964  zfcndrep 4966  suppsrlem 5221  suppsr2 5223  suppsr3 5224  hbnegd 5363  islp2 7747  cncnplem2 7775  qusp 10555

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

Copyright terms: Public domain