Theorem hbe1 1012

Description: x is not free in E.xph.

Assertion

Ref	Expression
hbe1	|- (E.xph -> A.xE.xph)

Proof of Theorem hbe1

Step	Hyp	Ref	Expression
1		hbn1 1011	. 2 |- (-. A.x -. ph -> A.x -. A.x -. ph)
2		df-ex 978	. 2 |- (E.xph <-> -. A.x -. ph)
3	2	albii 996	. 2 |- (A.xE.xph <-> A.x -. A.x -. ph)
4	1, 2, 3	3imtr4 219	1 |- (E.xph -> A.xE.xph)

Syntax hints:  -. wn 2   -> wi 3  A.wal 951  E.wex 977

This theorem is referenced by:  excomim 1041  19.23 1059  19.38 1077  exan 1102  hbmo1 1399  mopick2 1429  euor2 1430  moexex 1431  2moex 1433  2euex 1434  2moswap 1437  2exeu 1439  2eu4 1445  2eu7 1448  2eu8 1449  hbre1 1681  ceqsexg 1878  intab 2550  axrep1 2684  axrep2 2685  axrep3 2686  axrep4 2687  copsex2g 2783  mosubopt 2793  hbopab1 2802  hbopab2 2803  dfid3 2826  dmcosseq 3349  imadif 3560  hboprab1 3978  hboprab2 3979  zfcndrep 4938  zfcndpow 4940  zfcndreg 4941  zfcndinf 4942  suppsr3 5196

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

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978

Copyright terms: Public domain