Theorem bnj593 29862

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

Syntax hints:   → wi 4  ∃wex 1694

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

This theorem depends on definitions:  df-bi 195  df-ex 1695

This theorem is referenced by:  bnj1266  29929  bnj1304  29937  bnj1379  29948  bnj594  30029  bnj852  30038  bnj908  30048  bnj996  30072  bnj907  30082  bnj1128  30105  bnj1148  30111  bnj1154  30114  bnj1189  30124  bnj1245  30129  bnj1279  30133  bnj1286  30134  bnj1311  30139  bnj1371  30144  bnj1398  30149  bnj1408  30151  bnj1450  30165  bnj1498  30176  bnj1514  30178  bnj1501  30182