Theorem bnj593 34903

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

Syntax hints:   → wi 4  ∃wex 1781

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

This theorem depends on definitions:  df-bi 207  df-ex 1782

This theorem is referenced by:  bnj1266  34969  bnj1304  34977  bnj1379  34988  bnj594  35070  bnj852  35079  bnj908  35089  bnj996  35114  bnj907  35125  bnj1128  35148  bnj1148  35154  bnj1154  35157  bnj1189  35167  bnj1245  35172  bnj1279  35176  bnj1286  35177  bnj1311  35182  bnj1371  35187  bnj1398  35192  bnj1408  35194  bnj1450  35208  bnj1498  35219  bnj1514  35221  bnj1501  35225