Theorem hbe1 1016

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 1015	. 2 |- (-. A.x -. ph -> A.x -. A.x -. ph)
2		df-ex 981	. 2 |- (E.xph <-> -. A.x -. ph)
3	2	albii 999	. 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 954  E.wex 980

This theorem is referenced by:  excomim 1045  19.23 1063  19.38 1081  exan 1106  hbmo1 1406  mopick2 1436  euor2 1437  moexex 1438  2moex 1440  2euex 1441  2moswap 1444  2exeu 1446  2eu4 1452  2eu7 1455  2eu8 1456  hbre1 1689  ceqsexg 1887  intab 2560  axrep1 2694  axrep2 2695  axrep3 2696  axrep4 2697  copsex2g 2793  mosubopt 2804  hbopab1 2813  hbopab2 2814  dfid3 2836  dmcosseq 3365  imadif 3574  hboprab1 3993  hboprab2 3994  zfcndrep 4958  zfcndpow 4960  zfcndreg 4961  zfcndinf 4962  suppsr3 5216

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

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

Copyright terms: Public domain