Theorem bnj593 35443

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  35508  bnj1304  35516  bnj1379  35527  bnj594  35609  bnj852  35618  bnj908  35628  bnj996  35653  bnj907  35664  bnj1128  35687  bnj1148  35693  bnj1154  35696  bnj1189  35706  bnj1245  35711  bnj1279  35715  bnj1286  35716  bnj1311  35721  bnj1371  35726  bnj1398  35731  bnj1408  35733  bnj1450  35747  bnj1498  35758  bnj1514  35760  bnj1501  35764