Theorem bnj593 33744

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 206  df-ex 1782

This theorem is referenced by:  bnj1266  33810  bnj1304  33818  bnj1379  33829  bnj594  33911  bnj852  33920  bnj908  33930  bnj996  33955  bnj907  33966  bnj1128  33989  bnj1148  33995  bnj1154  33998  bnj1189  34008  bnj1245  34013  bnj1279  34017  bnj1286  34018  bnj1311  34023  bnj1371  34028  bnj1398  34033  bnj1408  34035  bnj1450  34049  bnj1498  34060  bnj1514  34062  bnj1501  34066