Theorem hba1 1350

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 73	. 2 |- (A.xph -> A.xph)
2	1	a5i 1335	1 |- (A.xph -> A.xA.xph)

Syntax hints:   -> wi 3  A.wal 1296

This theorem is referenced by:  hba2 1360  hbia1 1361  hbn1 1362  ax67to6 1368  ax467to6 1372  19.12 1394  19.21 1403  19.38 1432  19.21t 1473  19.23t 1474  exintr 1475  dvelimfALT 1514  sbf2 1552  sbiedOLD 1564  equs5a 1566  ax11v2 1585  equs5 1591  hbsb4t 1621  hbsb4tOLD 1622  sb56 1643  sbal1 1737  dvelimALT 1744  ax11eq 1754  ax11el 1755  ax11indalem 1759  ax11inda2ALT 1760  ax11inda 1762  a12study 1769  a12studyALT 1770  hbeu1 1781  hbeu 1782  moexex 1841  2eu1 1853  2eu4 1856  exists2 1863  hbra1 2147  hbra2 2148  ralcom2 2244  ralcom2OLD 2245  ceqsalg 2314  abidhb 2423  hbeqd 2424  hbeld 2425  hbsbc1gd 2515  hbsbc1gdOLD 2516  hbsbcgd 2517  hbsbcgdOLD 2518  sbcralt 2527  sbcrext 2528  sbcralgf 2529  sbcrexgf 2530  csbie2t 2578  csbnestglem 2580  csbnestg 2581  csbnest1g 2582  sbcnestg 2583  hbss 2614  hbopd 3169  intab 3247  hbbrdOLD 3383  axrep1 3429  axrep2 3430  axrep3 3431  axrep4 3432  moabex 3513  copsexg 3537  mosubopt 3551  ssopab2 3573  eualeqhb 3824  eualexeq 3825  euexeqOLD 3826  alxfr 3836  dmcosseqOLD 4215  hbimad 4275  hbfvd 4687  hbfvd2 4688  fv3 4690  cbvfo 4861  hboprdOLD 4906  fnoprabg 4941  pssnn 5628  fiint 5650  ordtypelem4 5687  hta 5858  aceq1 5891  zorn2lem4 5953  axrepndlem1 6096  axrepndlem2 6097  axunnd 6100  axpowndlem2 6102  axpowndlem3 6103  axpowndlem4 6104  axregndlem2 6107  axinfndlem1 6109  axinfnd 6110  axacndlem4 6114  axacndlem5 6115  axacnd 6116  zfcndrep 6118  suppsrlem 6373  suppsr2 6375  suppsr3 6376  hbnegdOLD 6519  islp2 9023  cncnplem2 9052  indexfi 10174  bnj9 12372  bnj32 12398  bnj1094 12914  dfon2lem7 13855  qusp 14908  inficlALT 15372  ordtypelem4OLD 15378  indexfiOLD 15755  pm10.55 16316  2albi 16330  ax10ext 16364  ax10-16 16365  iotain 16381  pm14.122b 16387  pm14.123b 16390  eupickbi 16400  eubi 16402  cla4gft 16406

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

Copyright terms: Public domain