Theorem bnj593 34943

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  35008  bnj1304  35016  bnj1379  35027  bnj594  35109  bnj852  35118  bnj908  35128  bnj996  35153  bnj907  35164  bnj1128  35187  bnj1148  35193  bnj1154  35196  bnj1189  35206  bnj1245  35211  bnj1279  35215  bnj1286  35216  bnj1311  35221  bnj1371  35226  bnj1398  35231  bnj1408  35233  bnj1450  35247  bnj1498  35258  bnj1514  35260  bnj1501  35264