Theorem bnj593 34928

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  34993  bnj1304  35001  bnj1379  35012  bnj594  35094  bnj852  35103  bnj908  35113  bnj996  35138  bnj907  35149  bnj1128  35172  bnj1148  35178  bnj1154  35181  bnj1189  35191  bnj1245  35196  bnj1279  35200  bnj1286  35201  bnj1311  35206  bnj1371  35211  bnj1398  35216  bnj1408  35218  bnj1450  35232  bnj1498  35243  bnj1514  35245  bnj1501  35249