Theorem bnj593 34760

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

Syntax hints:   → wi 4  ∃wex 1778

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

This theorem depends on definitions:  df-bi 207  df-ex 1779

This theorem is referenced by:  bnj1266  34826  bnj1304  34834  bnj1379  34845  bnj594  34927  bnj852  34936  bnj908  34946  bnj996  34971  bnj907  34982  bnj1128  35005  bnj1148  35011  bnj1154  35014  bnj1189  35024  bnj1245  35029  bnj1279  35033  bnj1286  35034  bnj1311  35039  bnj1371  35044  bnj1398  35049  bnj1408  35051  bnj1450  35065  bnj1498  35076  bnj1514  35078  bnj1501  35082