Theorem bnj593 34721

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

Syntax hints:   → wi 4  ∃wex 1777

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

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

This theorem is referenced by:  bnj1266  34787  bnj1304  34795  bnj1379  34806  bnj594  34888  bnj852  34897  bnj908  34907  bnj996  34932  bnj907  34943  bnj1128  34966  bnj1148  34972  bnj1154  34975  bnj1189  34985  bnj1245  34990  bnj1279  34994  bnj1286  34995  bnj1311  35000  bnj1371  35005  bnj1398  35010  bnj1408  35012  bnj1450  35026  bnj1498  35037  bnj1514  35039  bnj1501  35043