Theorem hbe1 1014

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 1013	. 2 |- (-. A.x -. ph -> A.x -. A.x -. ph)
2		df-ex 979	. 2 |- (E.xph <-> -. A.x -. ph)
3	2	albii 997	. 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 952  E.wex 978

This theorem is referenced by:  excomim 1043  19.23 1061  19.38 1079  exan 1104  hbmo1 1404  mopick2 1434  euor2 1435  moexex 1436  2moex 1438  2euex 1439  2moswap 1442  2exeu 1444  2eu4 1450  2eu7 1453  2eu8 1454  hbre1 1686  ceqsexg 1883  intab 2555  axrep1 2689  axrep2 2690  axrep3 2691  axrep4 2692  copsex2g 2788  mosubopt 2799  hbopab1 2808  hbopab2 2809  dfid3 2831  dmcosseq 3357  imadif 3566  hboprab1 3984  hboprab2 3985  zfcndrep 4946  zfcndpow 4948  zfcndreg 4949  zfcndinf 4950  suppsr3 5204

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-4 971  ax-5o 973  ax-6o 976

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

Copyright terms: Public domain