Theorem bnj593 32248

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

Syntax hints:   → wi 4  ∃wex 1781

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

This theorem depends on definitions:  df-bi 210  df-ex 1782

This theorem is referenced by:  bnj1266  32315  bnj1304  32323  bnj1379  32334  bnj594  32416  bnj852  32425  bnj908  32435  bnj996  32460  bnj907  32471  bnj1128  32494  bnj1148  32500  bnj1154  32503  bnj1189  32513  bnj1245  32518  bnj1279  32522  bnj1286  32523  bnj1311  32528  bnj1371  32533  bnj1398  32538  bnj1408  32540  bnj1450  32554  bnj1498  32565  bnj1514  32567  bnj1501  32571