Theorem bnj593 35043

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

Hypotheses

Ref	Expression
bnj593.1	⊢ (𝜑 → ∃𝑥𝜓)
bnj593.2	⊢ (𝜓 → 𝜒)

Assertion

Ref	Expression
bnj593	⊢ (𝜑 → ∃𝑥𝜒)

Proof of Theorem bnj593

Step	Hyp	Ref	Expression
1		bnj593.1	. 2 ⊢ (𝜑 → ∃𝑥𝜓)
2		bnj593.2	. . 3 ⊢ (𝜓 → 𝜒)
3	2	eximi 1857	. 2 ⊢ (∃𝑥𝜓 → ∃𝑥𝜒)
4	1, 3	syl 17	1 ⊢ (𝜑 → ∃𝑥𝜒)

Syntax hints:   → wi 4  ∃wex 1801

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

This theorem depends on definitions:  df-bi 209  df-ex 1802

This theorem is referenced by:  bnj1266  35108  bnj1304  35116  bnj1379  35127  bnj594  35209  bnj852  35218  bnj908  35228  bnj996  35253  bnj907  35264  bnj1128  35287  bnj1148  35293  bnj1154  35296  bnj1189  35306  bnj1245  35311  bnj1279  35315  bnj1286  35316  bnj1311  35321  bnj1371  35326  bnj1398  35331  bnj1408  35333  bnj1450  35347  bnj1498  35358  bnj1514  35360  bnj1501  35364