Theorem bnj593 35242

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

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

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

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

This theorem is used by:  bnj1266  35307  bnj1304  35315  bnj1379  35326  bnj594  35408  bnj852  35417  bnj908  35427  bnj996  35452  bnj907  35463  bnj1128  35486  bnj1148  35492  bnj1154  35495  bnj1189  35505  bnj1245  35510  bnj1279  35514  bnj1286  35515  bnj1311  35520  bnj1371  35525  bnj1398  35530  bnj1408  35532  bnj1450  35546  bnj1498  35557  bnj1514  35559  bnj1501  35563