Theorem bnj593 33787

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

Syntax hints:   → wi 4  ∃wex 1782

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

This theorem depends on definitions:  df-bi 206  df-ex 1783

This theorem is referenced by:  bnj1266  33853  bnj1304  33861  bnj1379  33872  bnj594  33954  bnj852  33963  bnj908  33973  bnj996  33998  bnj907  34009  bnj1128  34032  bnj1148  34038  bnj1154  34041  bnj1189  34051  bnj1245  34056  bnj1279  34060  bnj1286  34061  bnj1311  34066  bnj1371  34071  bnj1398  34076  bnj1408  34078  bnj1450  34092  bnj1498  34103  bnj1514  34105  bnj1501  34109