Theorem bnj593 30815

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)

Hypotheses

Ref	Expression
bnj593.1	|- ( ph -> E. x ps )
bnj593.2	|- ( ps -> ch )

Assertion

Ref	Expression
bnj593	|- ( ph -> E. x ch )

Proof of Theorem bnj593

Step	Hyp	Ref	Expression
1		bnj593.1	. 2 |- ( ph -> E. x ps )
2		bnj593.2	. . 3 |- ( ps -> ch )
3	2	eximi 1762	. 2 |- ( E. x ps -> E. x ch )
4	1, 3	syl 17	1 |- ( ph -> E. x ch )

Syntax hints:   -> wi 4   E.wex 1704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737

This theorem depends on definitions:  df-bi 197  df-ex 1705

This theorem is referenced by:  bnj1266  30882  bnj1304  30890  bnj1379  30901  bnj594  30982  bnj852  30991  bnj908  31001  bnj996  31025  bnj907  31035  bnj1128  31058  bnj1148  31064  bnj1154  31067  bnj1189  31077  bnj1245  31082  bnj1279  31086  bnj1286  31087  bnj1311  31092  bnj1371  31097  bnj1398  31102  bnj1408  31104  bnj1450  31118  bnj1498  31129  bnj1514  31131  bnj1501  31135