Theorem hbe1 1048

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 1047	. 2 |- (-. A.x -. ph -> A.x -. A.x -. ph)
2		df-ex 1013	. 2 |- (E.xph <-> -. A.x -. ph)
3	2	albii 1031	. 2 |- (A.xE.xph <-> A.x -. A.x -. ph)
4	1, 2, 3	3imtr4i 217	1 |- (E.xph -> A.xE.xph)

Syntax hints:  -. wn 2   -> wi 3  A.wal 986  E.wex 1012

This theorem is referenced by:  excomim 1077  19.23 1095  19.38 1113  exan 1138  hbmo1 1439  eupicka 1468  mopick2 1470  euor2 1471  moexex 1472  2moex 1474  2euex 1475  2moswap 1478  2exeu 1480  2eu4 1486  2eu7 1489  2eu8 1490  hbre1 1727  ceqsexg 1925  intab 2608  axrep1 2745  axrep2 2746  axrep3 2747  axrep4 2748  copsex2g 2846  mosubopt 2857  hbopab1 2866  hbopab2 2867  dfid3 2890  dmcosseq 3425  imadif 3649  hboprab1 4069  hboprab2 4070  zfcndrep 5055  zfcndpow 5057  zfcndreg 5058  zfcndinf 5059  suppsr3 5313  xfree 10489

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 995  ax-4 1005  ax-5o 1007  ax-6o 1010

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1013

Copyright terms: Public domain