Theorem hbe1 1363

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 1362	. 2 |- (-. A.x -. ph -> A.x -. A.x -. ph)
2		df-ex 1327	. 2 |- (E.xph <-> -. A.x -. ph)
3	2	albii 1346	. 2 |- (A.xE.xph <-> A.x -. A.x -. ph)
4	1, 2, 3	3imtr4i 236	1 |- (E.xph -> A.xE.xph)

Syntax hints:  -. wn 2   -> wi 3  A.wal 1296  E.wex 1326

This theorem is referenced by:  excomim 1392  19.23 1411  19.38 1432  exan 1463  exanOLD 1464  hbmo1 1802  euan 1827  eupicka 1835  mopick2 1837  mopick2OLD 1838  euor2 1839  euor2OLD 1840  moexex 1841  2moex 1843  2euex 1844  2euexOLD 1845  2moswap 1848  2exeu 1850  2eu4 1856  2eu7 1859  2eu8 1860  hbre1 2150  ceqsexg 2392  sbc6g 2472  intab 3247  axrep1 3429  axrep2 3430  axrep3 3431  axrep4 3432  copsexg 3537  copsex2g 3539  mosubopt 3551  hbopab1 3562  hbopab2 3563  dfid3 3587  euexeqOLD 3826  euexaleq 3827  dmcoss 4211  dmcosseqOLD 4215  imadif 4493  hboprab1 4919  hboprab2 4920  ordtype 5691  zfcndrep 6118  zfcndpow 6120  zfcndreg 6121  zfcndinf 6122  suppsr3 6376  xfree 12016  bnj1201 12978  bnj607 13304  bnj1398 13515  bnj1449 13539  exisym1 14248  finminlem 15367  inficlALT 15372  ordtypeOLD 15382  morex 15662  fsumltisumi 15823  fsumleisumi 15826

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

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327

Copyright terms: Public domain