Theorem bnj593 34941

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 1843	. 2 ⊢ (∃𝑥𝜓 → ∃𝑥𝜒)
4	1, 3	syl 17	1 ⊢ (𝜑 → ∃𝑥𝜒)

Syntax hints:   → wi 4  ∃wex 1787

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

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

This theorem is referenced by:  bnj1266  35006  bnj1304  35014  bnj1379  35025  bnj594  35107  bnj852  35116  bnj908  35126  bnj996  35151  bnj907  35162  bnj1128  35185  bnj1148  35191  bnj1154  35194  bnj1189  35204  bnj1245  35209  bnj1279  35213  bnj1286  35214  bnj1311  35219  bnj1371  35224  bnj1398  35229  bnj1408  35231  bnj1450  35245  bnj1498  35256  bnj1514  35258  bnj1501  35262