Theorem bnj593 35143

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

This proof depends on syntax axioms:   → wi 4  ∃wex 1808

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838

This proof depends on definitions:  df-bi 210  df-ex 1809

This theorem is used by:  bnj1266  35208  bnj1304  35216  bnj1379  35227  bnj594  35309  bnj852  35318  bnj908  35328  bnj996  35353  bnj907  35364  bnj1128  35387  bnj1148  35393  bnj1154  35396  bnj1189  35406  bnj1245  35411  bnj1279  35415  bnj1286  35416  bnj1311  35421  bnj1371  35426  bnj1398  35431  bnj1408  35433  bnj1450  35447  bnj1498  35458  bnj1514  35460  bnj1501  35464