Theorem bnj593 34888

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  34953  bnj1304  34961  bnj1379  34972  bnj594  35054  bnj852  35063  bnj908  35073  bnj996  35098  bnj907  35109  bnj1128  35132  bnj1148  35138  bnj1154  35141  bnj1189  35151  bnj1245  35156  bnj1279  35160  bnj1286  35161  bnj1311  35166  bnj1371  35171  bnj1398  35176  bnj1408  35178  bnj1450  35192  bnj1498  35203  bnj1514  35205  bnj1501  35209